Library zoo_std.condition

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  mutex
  condition__code.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types t pred : val.

Section mutex_G.
  Context `{mutex_G : MutexG Σ}.

  Definition condition_inv t : iProp Σ :=
    True.

  #[global] Instance condition_inv_persistent t :
    Persistent (condition_inv t).

  Lemma condition ٠ create 𑁒 spec :
    {{{
      True
    }}}
      condition ٠ create ()
    {{{
      t
    , RET t ;
      condition_inv t
    }}}.
  Lemma condition ٠ create 𑁒 diaspec :
    DIASPEC
    {{
      True
    }}
      condition ٠ create ()
    {{ t ,
      RET t ;
      condition_inv t
    }}.

  Lemma condition ٠ notify 𑁒 spec t :
    {{{
      condition_inv t
    }}}
      condition ٠ notify t
    {{{
      RET ();
      True
    }}}.
  Lemma condition ٠ notify 𑁒 diaspec t :
    DIASPEC
    {{
      condition_inv t
    }}
      condition ٠ notify t
    {{
      RET ();
      True
    }}.

  Lemma condition ٠ notify_all 𑁒 spec t :
    {{{
      condition_inv t
    }}}
      condition ٠ notify_all t
    {{{
      RET ();
      True
    }}}.
  #[global] Instance condition ٠ notify_all 𑁒 diaspec t :
    DIASPEC
    {{
      condition_inv t
    }}
      condition ٠ notify_all t
    {{
      RET ();
      True
    }}.

  Lemma condition ٠ wait 𑁒 spec t mtx P :
    {{{
      condition_inv t ∗
      mutex_inv mtx P ∗
      mutex_locked mtx ∗
      P
    }}}
      condition ٠ wait t mtx
    {{{
      RET ();
      mutex_locked mtx ∗
      P
    }}}.
  Lemma condition ٠ wait 𑁒 diaspec t mtx P :
    DIASPEC
    {{
      condition_inv t ∗
      mutex_inv mtx P ∗
      mutex_locked mtx ∗
      P
    }}
      condition ٠ wait t mtx
    {{
      RET ();
      mutex_locked mtx ∗
      P
    }}.

  Lemma condition ٠ wait_until 𑁒 spec' Ψ t mtx pred P :
    {{{
      condition_inv t ∗
      mutex_inv mtx P ∗
      mutex_locked mtx ∗
      P ∗
      Ψ false ∗
      □ (
        mutex_locked mtx -∗
        P -∗
        Ψ false -∗
        WP pred () {{ res ,
          ∃ b ,
          ⌜res = #b ⌝ ∗
          mutex_locked mtx ∗
          (if b then True else P ) ∗
          Ψ b
        }}
      )
    }}}
      condition ٠ wait_until t mtx pred
    {{{
      RET ();
      mutex_locked mtx ∗
      Ψ true
    }}}.
  Lemma condition ٠ wait_until 𑁒 spec Ψ t mtx pred P :
    {{{
      condition_inv t ∗
      mutex_inv mtx P ∗
      mutex_locked mtx ∗
      P ∗
      Ψ false ∗
      □ (
        mutex_locked mtx -∗
        P -∗
        Ψ false -∗
        WP pred () {{ res ,
          ∃ b ,
          ⌜res = #b ⌝ ∗
          mutex_locked mtx ∗
          P ∗
          Ψ b
        }}
      )
    }}}
      condition ٠ wait_until t mtx pred
    {{{
      RET ();
      mutex_locked mtx ∗
      P ∗
      Ψ true
    }}}.

  Lemma condition ٠ wait_while 𑁒 spec' Ψ t mtx pred P :
    {{{
      condition_inv t ∗
      mutex_inv mtx P ∗
      mutex_locked mtx ∗
      P ∗
      Ψ true ∗
      □ (
        mutex_locked mtx -∗
        P -∗
        Ψ true -∗
        WP pred () {{ res ,
          ∃ b ,
          ⌜res = #b ⌝ ∗
          mutex_locked mtx ∗
          (if b then P else True ) ∗
          Ψ b
        }}
      )
    }}}
      condition ٠ wait_while t mtx pred
    {{{
      RET ();
      mutex_locked mtx ∗
      Ψ false
    }}}.
  Lemma condition ٠ wait_while 𑁒 spec Ψ t mtx pred P :
    {{{
      condition_inv t ∗
      mutex_inv mtx P ∗
      mutex_locked mtx ∗
      P ∗
      Ψ true ∗
      □ (
        mutex_locked mtx -∗
        P -∗
        Ψ true -∗
        WP pred () {{ res ,
          ∃ b ,
          ⌜res = #b ⌝ ∗
          mutex_locked mtx ∗
          P ∗
          Ψ b
        }}
      )
    }}}
      condition ٠ wait_while t mtx pred
    {{{
      RET ();
      mutex_locked mtx ∗
      P ∗
      Ψ false
    }}}.
End mutex_G.

From zoo_std Require
  condition__opaque.

#[global] Opaque condition_inv.