Library zoo_std.mutex

Require Import zoo.prelude.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.base.
Require Export zoo_std.mutex__code.
Require Import zoo_std.mutex__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type l : location.
Implicit Type t fn : val.

Class MutexG Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] mutex ۰ G ۰ excl ۰ G :: ExclG Σ unitO
  }.

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

Section mutex ۰ G.
  Context `{mutex ۰ G : MutexG Σ}.

  #[local] Definition metadata :=
    gname.
  Implicit Type γ : metadata.

  #[local] Definition locked γ :=
    excl γ ().

  Definition mutex ۰ init t b : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    l ↦ᵣ #b ∗
    if b then True else locked γ.

  #[local] Definition inv ۰ inner l γ P : iProp Σ :=
    ∃ b ,
    l ↦ᵣ #b ∗
    match b with
    | true ⇒
        True
    | false ⇒
        locked γ ∗
        P
    end.
  Definition mutex ۰ inv t P : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    inv nroot (inv ۰ inner l γ P).

  Definition mutex ۰ locked t : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    locked γ.

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

  #[global] Instance mutex ۰ init ｰ timeless t b :
    Timeless (mutex ۰ init t b).
  #[global] Instance mutex ۰ locked ｰ timeless t :
    Timeless (mutex ۰ locked t).

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

  Lemma mutex ۰ init ｰ exclusive t b1 b2 :
    mutex ۰ init t b1 -∗
    mutex ۰ init t b2 -∗
    False.
  Lemma mutex ۰ init ｰ to ｰ inv {t b} P E :
    mutex ۰ init t b -∗
    (if b then True else ▷ P ) ={E }=∗
    mutex ۰ inv t P.

  Lemma mutex ۰ locked ｰ exclusive t :
    mutex ۰ locked t -∗
    mutex ۰ locked t -∗
    False.

  Lemma mutex ٠ create ｰ spec ｰ init :
    {{{
      True
    }}}
      mutex ٠ create ()
    {{{
      t
    , RET t ;
      mutex ۰ init t false
    }}}.
  Lemma mutex ٠ create ｰ spec P :
    {{{
      P
    }}}
      mutex ٠ create ()
    {{{
      t
    , RET t ;
      mutex ۰ inv t P
    }}}.

  Lemma mutex ٠ create_lock ｰ spec ｰ init :
    {{{
      True
    }}}
      mutex ٠ create_lock ()
    {{{
      t
    , RET t ;
      mutex ۰ init t true ∗
      mutex ۰ locked t
    }}}.
  Lemma mutex ٠ create_lock ｰ spec P :
    {{{
      True
    }}}
      mutex ٠ create_lock ()
    {{{
      t
    , RET t ;
      mutex ۰ inv t P ∗
      mutex ۰ locked t
    }}}.

  Lemma mutex ٠ lock ｰ spec t P :
    {{{
      mutex ۰ inv t P
    }}}
      mutex ٠ lock t
    {{{
      RET ();
      mutex ۰ locked t ∗
      P
    }}}.
  Lemma mutex ٠ lock ｰ spec ｰ init t :
    {{{
      mutex ۰ init t false
    }}}
      mutex ٠ lock t
    {{{
      RET ();
      mutex ۰ init t true ∗
      mutex ۰ locked t
    }}}.

  Lemma mutex ٠ unlock ｰ spec t P :
    {{{
      mutex ۰ inv t P ∗
      mutex ۰ locked t ∗
      P
    }}}
      mutex ٠ unlock t
    {{{
      RET ();
      True
    }}}.
  Lemma mutex ٠ unlock ｰ spec ｰ init t :
    {{{
      mutex ۰ init t true ∗
      mutex ۰ locked t
    }}}
      mutex ٠ unlock t
    {{{
      RET ();
      mutex ۰ init t false
    }}}.

  Lemma mutex ٠ synchronize ｰ spec t P :
    {{{
      mutex ۰ inv t P
    }}}
      mutex ٠ synchronize t
    {{{
      RET ();
      True
    }}}.
  #[global] Instance mutex ٠ synchronize ｰ diaspec t P :
    DIASPEC
    {{
      mutex ۰ inv t P
    }}
      mutex ٠ synchronize t
    {{
      RET ();
      True
    }}.

  Lemma mutex ٠ protect ｰ spec Ψ t P fn :
    {{{
      mutex ۰ inv t P ∗
      ( mutex ۰ locked t -∗
        P -∗
        WP fn () {{ v ,
          mutex ۰ locked t ∗
          P ∗
          Ψ v
        }}
      )
    }}}
      mutex ٠ protect t fn
    {{{
      v
    , RET v ;
      Ψ v
    }}}.
End mutex ۰ G.

Require zoo_std.mutex__opaque.

#[global] Opaque mutex ۰ init.
#[global] Opaque mutex ۰ inv.
#[global] Opaque mutex ۰ locked.