two more styles of lock spec

theories/locks/lockspecs/atomic_lock.v

+From iris.proofmode Require Import proofmode.
+From iris.base_logic.lib Require Export invariants ghost_var.
+From iris.bi.lib Require Import fractional.
+From iris.heap_lang Require Import proofmode primitive_laws notation atomic_heap.
+From iris.prelude Require Import options.
+
+(** Deallocatable lock with share, operations are atomic. *)
+Structure atomic_lock `{!heapGS Σ} := AtomicLock {
+  (** * Operations *)
+  newlock : val;
+  acquire : val;
+  release : val;
+  freelock : val;
+  (** * Predicates *)
+  (** [name] is used to associate locked with [is_lock] *)
+  name : Type;
+  (** No namespace [N] parameter because we only expose program specs, which
+  anyway have the full mask. *)
+  is_lock (f: Qp) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
+  locked (γ: name) : iProp Σ;
+  (** * General properties of the predicates *)
+  is_lock_ne f γ lk : Contractive (is_lock f γ lk);
+  is_lock_persistent γ lk R : Fractional (fun f => is_lock f γ lk R);
+  is_lock_iff f γ lk R1 R2 :
+    is_lock f γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock f γ lk R2;
+  locked_timeless γ : Timeless (locked γ);
+  locked_exclusive γ : locked γ -∗ locked γ -∗ False;
+  (** * Program specs *)
+  newlock_spec (R : iProp Σ) :
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock 1 γ lk R }}};
+  acquire_spec f γ (lk : val) R :
+    ⊢ <<{ is_lock f γ lk R }>> acquire lk @ ∅ <<{ is_lock f γ lk R ∗ locked γ ∗ R | RET #() }>>;
+  release_spec f γ lk R :
+    {{{ is_lock f γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); is_lock f γ lk R }}};
+  freelock_spec γ lk (R : iProp Σ) :
+    {{{ is_lock 1 γ lk R ∗ R }}} freelock #() {{{ RET #(); R }}}
+}.
+
+Inductive state := Free | Locked.
+
+Class lockG Σ := LockG { lock_tokG : ghost_varG Σ state }.
+Local Existing Instance lock_tokG.
+Definition lockΣ : gFunctors := #[ghost_varΣ state].
+Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. solve_inG. Qed.
+
+Section tada.
+  Context `{!heapGS Σ, !lockG Σ} (l : atomic_lock).
+
+  Record tada_lock_name := TadaLockName {
+    tada_lock_name_state : gname;
+    tada_lock_name_lock : l.(name);
+  }.
+
+  Definition tada_is_lock (γ : tada_lock_name) (lk : val) : iProp Σ :=
+    l.(is_lock) 1 γ.(tada_lock_name_lock) lk
+      (ghost_var γ.(tada_lock_name_state) (1/4) Free).
+  Definition tada_lock_state (γ : tada_lock_name) (lk : val) (s : state) : iProp Σ :=
+    tada_is_lock γ lk ∗ ghost_var γ.(tada_lock_name_state) (3/4) s ∗
+    if s is Locked then
+      l.(locked) γ.(tada_lock_name_lock) ∗ ghost_var γ.(tada_lock_name_state) (1/4) Locked
+    else True.
+
+(*  Global Instance tada_is_lock_persistent γ lk : Persistent (tada_is_lock γ lk).
+  Proof. apply _. Qed. *)
+(*  Global Instance tada_lock_state_timeless γ s : Timeless (tada_lock_state γ lk s).
+  Proof. destruct s; apply _. Qed.*)
+
+  Lemma tada_lock_state_exclusive γ lk s1 s2 :
+    tada_lock_state γ lk s1 -∗ tada_lock_state γ lk s2 -∗ False.
+  Proof.
+    iIntros "[_ [Hvar1 _]] [_ [Hvar2 _]]".
+    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[Hval _].
+    exfalso. done.
+  Qed.
+
+  Lemma newlock_tada_spec :
+    {{{ True }}}
+      l.(newlock) #()
+    {{{ lk γ, RET lk; tada_lock_state γ lk Free }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ".
+    iMod (ghost_var_alloc Free) as (γvar) "Hvar".
+    rewrite -Qp.three_quarter_quarter.
+    iDestruct "Hvar" as "[Hvar1 Hvar2]".
+    wp_apply (l.(newlock_spec) with "Hvar2").
+    iIntros (lk γlock) "Hlock".
+    iApply ("HΦ" $! lk (TadaLockName _ _)).
+    iFrame.
+  Qed.
+
+  Lemma acquire_tada_spec γ (lk : val) :
+    ⊢<<{ ∀ s, tada_lock_state γ lk s }>>
+      l.(acquire) lk @ ∅
+    <<{ tada_lock_state γ lk Locked | RET #() }>>.
+  Proof.
+    iIntros "%Φ AU".
+    iApply fupd_wp.
+  Abort.
+
+  Lemma release_tada_spec γ (lk : val) :
+    ⊢<<{ tada_lock_state γ lk Locked }>>
+      l.(release) lk @ ∅
+    <<{ tada_lock_state γ lk Free | RET #() }>>.
+  Proof.
+  Abort.
+
+End tada.

theories/locks/lockspecs/share_locks.v

+From iris.base_logic.lib Require Export invariants ghost_var.
+From iris.bi.lib Require Import fractional.
+From iris.heap_lang Require Import primitive_laws notation proofmode atomic_heap.
+From iris.prelude Require Import options.
+
+(** Deallocatable lock with share. *)
+Structure lock `{!heapGS Σ} := Lock {
+  (** * Operations *)
+  newlock : val;
+  acquire : val;
+  release : val;
+  freelock : val;
+  (** * Predicates *)
+  (** [name] is used to associate locked with [is_lock] *)
+  name : Type;
+  (** No namespace [N] parameter because we only expose program specs, which
+  anyway have the full mask. *)
+  is_lock (f: Qp) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
+  locked (γ: name) : iProp Σ;
+  (** * General properties of the predicates *)
+  is_lock_ne f γ lk : Contractive (is_lock f γ lk);
+  is_lock_persistent γ lk R : Fractional (fun f => is_lock f γ lk R);
+  is_lock_iff f γ lk R1 R2 :
+    is_lock f γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock f γ lk R2;
+  locked_timeless γ : Timeless (locked γ);
+  locked_exclusive γ : locked γ -∗ locked γ -∗ False;
+  (** * Program specs *)
+  newlock_spec (R : iProp Σ) :
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock 1 γ lk R }}};
+  acquire_spec f γ lk R :
+    {{{ is_lock f γ lk R }}} acquire lk {{{ RET #(); is_lock f γ lk R ∗ locked γ ∗ R }}};
+  release_spec f γ lk R :
+    {{{ is_lock f γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); is_lock f γ lk R }}};
+  freelock_spec γ lk (R : iProp Σ) :
+    {{{ is_lock 1 γ lk R ∗ R }}} freelock #() {{{ RET #(); R }}}
+}.
+
+Inductive state := Free | Locked.
+
+Class lockG Σ := LockG { lock_tokG : ghost_varG Σ state }.
+Local Existing Instance lock_tokG.
+Definition lockΣ : gFunctors := #[ghost_varΣ state].
+Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. solve_inG. Qed.
+
+Section tada.
+  Context `{!heapGS Σ, !lockG Σ} (l : lock).
+
+  Record tada_lock_name := TadaLockName {
+    tada_lock_name_state : gname;
+    tada_lock_name_lock : l.(name);
+  }.
+
+  Definition tada_is_lock f (γ : tada_lock_name) (lk : val) : iProp Σ :=
+    l.(is_lock) f γ.(tada_lock_name_lock) lk
+      (ghost_var γ.(tada_lock_name_state) (1/4) Free).
+  Definition tada_lock_state f (γ : tada_lock_name) (lk : val) (s : state) : iProp Σ :=
+    tada_is_lock f γ lk ∗ ghost_var γ.(tada_lock_name_state) (3/4) s ∗
+    if s is Locked then
+      l.(locked) γ.(tada_lock_name_lock) ∗ ghost_var γ.(tada_lock_name_state) (1/4) Locked
+    else True.
+
+  Lemma tada_lock_state_exclusive f1 f2 γ lk s1 s2 :
+    tada_lock_state f1 γ lk s1 -∗ tada_lock_state f2 γ lk s2 -∗ False.
+  Proof.
+    iIntros "[_ [Hvar1 _]] [_ [Hvar2 _]]".
+    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[Hval _].
+    exfalso. done.
+  Qed.
+
+  Lemma newlock_tada_spec :
+    {{{ True }}}
+      l.(newlock) #()
+    {{{ lk γ, RET lk; tada_lock_state 1 γ lk Free }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ".
+    iMod (ghost_var_alloc Free) as (γvar) "Hvar".
+    rewrite -{2}Qp.three_quarter_quarter.
+    iDestruct "Hvar" as "[Hvar1 Hvar2]".
+    wp_apply (l.(newlock_spec) with "Hvar2").
+    iIntros (lk γlock) "Hlock".
+    iApply ("HΦ" $! lk (TadaLockName _ _)).
+    iFrame.
+  Qed.
+
+  Lemma acquire_tada_spec f γ (lk : val) :
+    ⊢<<{ ∀ s, tada_lock_state f γ lk s }>>
+      l.(acquire) lk @ ∅
+    <<{ tada_lock_state f γ lk Locked | RET #() }>>.
+  Proof.
+    iIntros "%Φ AU".
+    iApply fupd_wp.
+    iMod "AU" as "[Hislock [Hclose _]]".
+    (* we have l.(is_lock), but have to return it before applying l.(acquire_spec) --
+       probably need the loan trick from freeable_logatom_lock *)
+    iMod ("Hclose" with "[$Hislock]") as "AU".
+    iModIntro.
+    iApply wp_fupd.
+    wp_apply (l.(acquire_spec)).
+(*    iIntros "[Hlocked Hvar1]".
+    iMod "AU" as (s) "[[_ [Hvar2 _]] [_ Hclose]]".
+    iDestruct (ghost_var_agree with "Hvar1 Hvar2") as %<-.
+    iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
+    { admit. }
+    iMod ("Hclose" with "[$Hislock $Hvar2 $Hlocked $Hvar1]"). done.
+  Qed.*)
+  Abort.
+
+End tada.