Library zoo_std.semaphore

From stdpp Require Import
  finite.

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.bi Require Import
  big_op.
From zoo.iris.base_logic Require Import
  lib.excl.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  semaphore__code.
From zoo_std Require Import
  semaphore__types
  condition.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types cnt : nat.
Implicit Types l : location.
Implicit Types 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 Types P : iProp Σ.

  Record metadata :=
    { metadata_mutex : val
    ; metadata_condition : val
    ; metadata_tokens : list gname
    }.
  Implicit Types γ : metadata.
  Implicit Types γ_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 (S cnt),
      tokens_frag γ ∗
      P.
  #[local] Instance : CustomIpat "inv_inner" :=
    " ( %cnt & Hl_count & H ) ".
  Definition semaphore_inv t cap P : iProp Σ :=
    ∃ l γ,
    ⌜t = #l⌝ ∗
    meta l nroot γ ∗
    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⌝ ∗
    meta l nroot γ ∗
    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.

From zoo_std Require
  semaphore__opaque.

#[global] Opaque semaphore_inv.
#[global] Opaque semaphore_locked.