Library zoo_std.condition

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.mutex.
Require Export zoo_std.condition__code.
Require Import zoo_std.condition__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type 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.

Require zoo_std.condition__opaque.

#[global] Opaque condition ۰ inv.