Library zoo_std.semaphore

Require Import stdpp.finite.

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.base.
Require Export zoo_std.semaphore__code.
Require Import zoo_std.semaphore__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type cnt : nat.
Implicit Type l : location.
Implicit Type t : val.

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

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

Section semaphore ۰ G.
  Context `{semaphore ۰ G : SemaphoreG Σ}.

  Implicit Type P : iProp Σ.

  Record metadata :=
    { metadata ۰ mutex : val
    ; metadata ۰ condition : val
    ; metadata ۰ tokens : list gname
    }.
  Implicit Type γ : metadata.
  Implicit Type γ_tokens : list gname.

  #[local] Instance metadata ｰ eq_dec : EqDecision metadata :=
    ltac:(solve_decision).
  #[local] Instance metadata ｰ countable :
    Countable metadata.

  #[local] Definition tokens ۰ auth' γ_tokens cap : iProp Σ :=
    ⌜length γ_tokens = cap ⌝.
  #[local] Definition tokens ۰ auth γ :=
    tokens ۰ auth' γ.(metadata ۰ tokens).
  #[local] Instance : CustomIpat "tokens۰auth" :=
    " %Htokens ".
  #[local] Definition tokens ۰ frag' γ_tokens : iProp Σ :=
    ∃ i η ,
    ⌜γ_tokens !! i = Some η ⌝ ∗
    excl η ().
  #[local] Definition tokens ۰ frag γ :=
    tokens ۰ frag' γ.(metadata ۰ tokens).
  #[local] Instance : CustomIpat "tokens۰frag" :=
    " ( %i & %η & %Htokens_lookup & Hexcl ) ".

  #[local] Definition inv ۰ inner l γ P : iProp Σ :=
    ∃ cnt ,
    l .[count ] ↦ #cnt ∗
    [∗ list ] _ ∈ seq 0 ˖cnt ,
      tokens ۰ frag γ ∗
      P.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %cnt & Hl_count & H ) ".
  Definition semaphore ۰ inv t cap P : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    l .[mutex ] ↦□ γ.(metadata ۰ mutex) ∗
    mutex ۰ inv γ.(metadata ۰ mutex) (inv ۰ inner l γ P) ∗
    l .[condition ] ↦□ γ.(metadata ۰ condition) ∗
    condition ۰ inv γ.(metadata ۰ condition) ∗
    tokens ۰ auth γ cap.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & -> & #Hmeta & #Hl_mutex & #Hmutex_inv & #Hl_condition & #Hcondition_inv & #Htokens_auth ) ".

  Definition semaphore ۰ locked t : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    tokens ۰ frag γ.
  #[local] Instance : CustomIpat "locked" :=
    " ( %l_ & %γ_ & %Heq & #Hmeta_ & Htokens_frag ) ".

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

  #[global] Instance semaphore ۰ locked ｰ timeless t :
    Timeless (semaphore ۰ locked t).

  #[local] Instance tokens ۰ auth ｰ persistent γ cap :
    Persistent (tokens ۰ auth γ cap).
  #[global] Instance semaphore ۰ inv ｰ persistent t cap P :
    Persistent (semaphore ۰ inv t cap P).

  #[local] Lemma tokens ｰ alloc cap :
    ⊢ |==>
      ∃ γ_tokens ,
      tokens ۰ auth' γ_tokens cap ∗
      [∗ list ] _ ∈ seq 0 cap , tokens ۰ frag' γ_tokens.
  #[local] Lemma tokens ۰ frags ｰ valid γ cap n :
    tokens ۰ auth γ cap -∗
    ([∗ list ] _ ∈ seq 0 n , tokens ۰ frag γ ) -∗
    ⌜n ≤ cap ⌝.

  Opaque tokens ۰ auth.
  Opaque tokens ۰ frag.

  Lemma semaphore ٠ create ｰ spec {cap} P :
    (0 < cap)%Z →
    {{{
      [∗ list ] _ ∈ seq 0 ₊cap , P
    }}}
      semaphore ٠ create #cap
    {{{
      t
    , RET t ;
      semaphore ۰ inv t ₊cap P
    }}}.

  Lemma semaphore ٠ try_lock ｰ spec t cap P :
    {{{
      semaphore ۰ inv t cap P
    }}}
      semaphore ٠ try_lock t
    {{{
      b
    , RET #b ;
      if b then
        semaphore ۰ locked t ∗
        P
      else
        True
    }}}.

  Lemma semaphore ٠ lock ｰ spec t cap P :
    {{{
      semaphore ۰ inv t cap P
    }}}
      semaphore ٠ lock t
    {{{
      RET ();
      semaphore ۰ locked t ∗
      P
    }}}.

  Lemma semaphore ٠ unlock ｰ spec t cap P :
    {{{
      semaphore ۰ inv t cap P ∗
      semaphore ۰ locked t ∗
      P
    }}}
      semaphore ٠ unlock t
    {{{
      RET ();
      True
    }}}.
End semaphore ۰ G.

Require zoo_std.semaphore__opaque.

#[global] Opaque semaphore ۰ inv.
#[global] Opaque semaphore ۰ locked.