two more styles of lock spec

Added two more styles of lock spec with explicit share; I believe they can be proved equivalent to the existing ones, but I don't have the proofs.

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.

[Ralf Jung]

This should be called _fractional

[Ralf Jung]

Please add some more comments explaining what is happening here... I think the point of this is just to implement the interface? It's confusing that the interface does not mention TaDA but the implementation does.

It might also be worth saying how this relates to iris_heap_lang/lib/logatom_lock.v, since there's clearly some overlap.

[Ralf Jung]

Please don't keep commented-out code around.