From 6aa1559d97ee728ec6aac95010508f998f3a5fc7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Aug 2023 11:06:14 +0200
Subject: [PATCH] =?UTF-8?q?fix=20lock=20spec=20code=20depending=20on=20?=
 =?UTF-8?q?=CE=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris_heap_lang/lib/lock.v         | 52 ++++++++++++++++++-------------
 iris_heap_lang/lib/logatom_lock.v |  8 ++---
 iris_heap_lang/lib/spin_lock.v    | 21 ++++++++-----
 iris_heap_lang/lib/ticket_lock.v  | 11 ++++---
 tests/heap_lang.v                 | 30 ++++++++++++++++--
 5 files changed, 82 insertions(+), 40 deletions(-)

diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index 5c66f9c7c..a7ba1b213 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -8,42 +8,52 @@ All parameters are implicit, since it is expected that there is only one
 [heapGS_gen] in scope that could possibly apply.
 
 Only one instance of this class should ever be in scope. To write a library that
-is generic over the lock, just add a [`{lock}] implicit parameter. To use a
-particular lock instance, use [Local Existing Instance <lock instance>].
+is generic over the lock, just add a [`{!lock}] implicit parameter around the
+code and [`{!lockG Î£}] around the proofs. To use a particular lock instance, use
+[Local Existing Instance <lock instance>].
 
 When writing an instance of this class, please take care not to shadow the class
 projections (e.g., either use [Local Definition newlock] or avoid the name
 [newlock] altogether), and do not register an instance -- just make it a
 [Definition] that others can register later. *)
-Class lock `{!heapGS_gen hlc Î£} := Lock {
+Class lock := Lock {
   (** * Operations *)
   newlock : val;
   acquire : val;
   release : val;
-  (** * Predicates *)
-  (** [name] is used to associate locked with [is_lock] *)
+  (** * Ghost state *)
+  (** The assumptions about [Î£] *)
+  lockG : gFunctors â†’ Type;
+  (** [name] is used to associate [locked] with [is_lock] *)
   lock_name : Type;
+  (** * Predicates *)
   (** No namespace [N] parameter because we only expose program specs, which
   anyway have the full mask. *)
-  is_lock (Î³: lock_name) (lock: val) (R: iProp Î£) : iProp Î£;
-  locked (Î³: lock_name) : iProp Î£;
+  is_lock `{!heapGS_gen hlc Î£} {L : lockG Î£} (Î³: lock_name) (lock: val) (R: iProp Î£) : iProp Î£;
+  locked `{!heapGS_gen hlc Î£} {L : lockG Î£} (Î³: lock_name) : iProp Î£;
   (** * General properties of the predicates *)
-  is_lock_persistent Î³ lk R :> Persistent (is_lock Î³ lk R);
-  is_lock_iff Î³ lk R1 R2 :
-    is_lock Î³ lk R1 -âˆ— â–· â–¡ (R1 âˆ—-âˆ— R2) -âˆ— is_lock Î³ lk R2;
-  locked_timeless Î³ :> Timeless (locked Î³);
-  locked_exclusive Î³ : locked Î³ -âˆ— locked Î³ -âˆ— False;
+  is_lock_persistent `{!heapGS_gen hlc Î£} {L : lockG Î£} Î³ lk R :>
+    Persistent (is_lock (L:=L) Î³ lk R);
+  is_lock_iff `{!heapGS_gen hlc Î£} {L : lockG Î£} Î³ lk R1 R2 :
+    is_lock (L:=L) Î³ lk R1 -âˆ— â–· â–¡ (R1 âˆ—-âˆ— R2) -âˆ— is_lock (L:=L) Î³ lk R2;
+  locked_timeless `{!heapGS_gen hlc Î£} {L : lockG Î£} Î³ :>
+    Timeless (locked (L:=L) Î³);
+  locked_exclusive `{!heapGS_gen hlc Î£} {L : lockG Î£} Î³ :
+    locked (L:=L) Î³ -âˆ— locked (L:=L) Î³ -âˆ— False;
   (** * Program specs *)
-  newlock_spec (R : iProp Î£) :
-    {{{ R }}} newlock #() {{{ lk Î³, RET lk; is_lock Î³ lk R }}};
-  acquire_spec Î³ lk R :
-    {{{ is_lock Î³ lk R }}} acquire lk {{{ RET #(); locked Î³ âˆ— R }}};
-  release_spec Î³ lk R :
-    {{{ is_lock Î³ lk R âˆ— locked Î³ âˆ— R }}} release lk {{{ RET #(); True }}}
+  newlock_spec `{!heapGS_gen hlc Î£} {L : lockG Î£} (R : iProp Î£) :
+    {{{ R }}} newlock #() {{{ lk Î³, RET lk; is_lock (L:=L) Î³ lk R }}};
+  acquire_spec `{!heapGS_gen hlc Î£} {L : lockG Î£} Î³ lk R :
+    {{{ is_lock (L:=L) Î³ lk R }}} acquire lk {{{ RET #(); locked (L:=L) Î³ âˆ— R }}};
+  release_spec `{!heapGS_gen hlc Î£} {L : lockG Î£} Î³ lk R :
+    {{{ is_lock (L:=L) Î³ lk R âˆ— locked (L:=L) Î³ âˆ— R }}} release lk {{{ RET #(); True }}}
 }.
-Global Hint Mode lock + + + : typeclass_instances.
 
-Global Instance is_lock_contractive `{!heapGS_gen hlc Î£, !lock} Î³ lk :
+Existing Class lockG.
+Global Hint Mode lockG + + : typeclass_instances.
+Global Hint Extern 0 (lockG _) => progress simpl : typeclass_instances.
+
+Global Instance is_lock_contractive `{!heapGS_gen hlc Î£, !lock, !lockG Î£} Î³ lk :
   Contractive (is_lock Î³ lk).
 Proof.
   apply (uPred.contractive_internal_eq (M:=iResUR Î£)).
@@ -52,5 +62,5 @@ Proof.
     iNext; iRewrite "HPQ"; auto.
 Qed.
 
-Global Instance is_lock_proper `{!heapGS_gen hlc Î£, !lock} Î³ lk :
+Global Instance is_lock_proper `{!heapGS_gen hlc Î£, !lock, !lockG Î£} Î³ lk :
   Proper ((â‰¡) ==> (â‰¡)) (is_lock Î³ lk) := ne_proper _.
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index e2cddb9ee..859fea3d5 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -18,14 +18,14 @@ From iris.prelude Require Import options.
 
 Inductive state := Free | Locked.
 
-Class lockG Î£ := LockG { lock_tokG : ghost_varG Î£ state }.
+Class alockG Î£ := LockG { lock_tokG : ghost_varG Î£ state }.
 Local Existing Instance lock_tokG.
-Definition lockÎ£ : gFunctors := #[ghost_varÎ£ state].
-Global Instance subG_lockÎ£ {Î£} : subG lockÎ£ Î£ â†’ lockG Î£.
+Definition alockÎ£ : gFunctors := #[ghost_varÎ£ state].
+Global Instance subG_alockÎ£ {Î£} : subG alockÎ£ Î£ â†’ alockG Î£.
 Proof. solve_inG. Qed.
 
 Section tada.
-  Context `{!heapGS Î£, !lockG Î£, !lock}.
+  Context `{!heapGS Î£, !alockG Î£, !lock, !lockG Î£}.
 
   Record tada_lock_name := TadaLockName {
     tada_lock_name_state : gname;
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 8686e3e03..9055ad138 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -14,16 +14,16 @@ Local Definition release : val := Î»: "l", "l" <- #false.
 
 (** The CMRA we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class lockG Î£ := LockG { lock_tokG : inG Î£ (exclR unitO) }.
+Class spin_lockG Î£ := LockG { lock_tokG : inG Î£ (exclR unitO) }.
 Local Existing Instance lock_tokG.
 
-Definition lockÎ£ : gFunctors := #[GFunctor (exclR unitO)].
+Definition spin_lockÎ£ : gFunctors := #[GFunctor (exclR unitO)].
 
-Global Instance subG_lockÎ£ {Î£} : subG lockÎ£ Î£ â†’ lockG Î£.
+Global Instance subG_spin_lockÎ£ {Î£} : subG spin_lockÎ£ Î£ â†’ spin_lockG Î£.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapGS_gen hlc Î£, !lockG Î£}.
+  Context `{!heapGS_gen hlc Î£, !spin_lockG Î£}.
   Let N := nroot .@ "spin_lock".
 
   Local Definition lock_inv (Î³ : gname) (l : loc) (R : iProp Î£) : iProp Î£ :=
@@ -92,7 +92,12 @@ Section proof.
   Qed.
 End proof.
 
-Definition spin_lock `{!heapGS_gen hlc Î£, !lockG Î£} : lock :=
-  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
-     lock.newlock_spec := newlock_spec;
-     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
+(* NOT an instance because users should choose explicitly to use it
+     (using [Explicit Instance]). *)
+Definition spin_lock : lock :=
+  {| lock.lockG := spin_lockG;
+     lock.locked_exclusive _ _ _ _ := locked_exclusive;
+     lock.is_lock_iff _ _ _ _ := is_lock_iff;
+     lock.newlock_spec _ _ _ _ := newlock_spec;
+     lock.acquire_spec _ _ _ _ := acquire_spec;
+     lock.release_spec _ _ _ _ := release_spec |}.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 02c4e48d0..0f9f1f47d 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -163,7 +163,10 @@ Section proof.
   Qed.
 End proof.
 
-Definition ticket_lock `{!heapGS_gen hlc Î£, !tlockG Î£} : lock :=
-  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
-     lock.newlock_spec := newlock_spec;
-     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
+Definition ticket_lock : lock :=
+  {| lock.lockG := tlockG;
+     lock.locked_exclusive _ _ _ _ := locked_exclusive;
+     lock.is_lock_iff _ _ _ _ := is_lock_iff;
+     lock.newlock_spec _ _ _ _ := newlock_spec;
+     lock.acquire_spec _ _ _ _ := acquire_spec;
+     lock.release_spec _ _ _ _ := release_spec |}.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 96d71b08b..c5f966bb0 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation lib.lock.
+From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation lib.spin_lock.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
@@ -516,7 +516,7 @@ Qed.
 
 (** Just making sure the lock typeclass actually works. *)
 Section lock.
-  Context `{!heapGS Î£, !lock}.
+  Context `{!lock}.
 
   Definition lock_client : val :=
     Î»: "loc" "lock",
@@ -524,6 +524,8 @@ Section lock.
       "loc" <- #42;;
       release "lock".
 
+  Context `{!heapGS Î£, !lockG Î£}.
+
   Lemma wp_lock_client loc lock Î³ :
     is_lock Î³ lock (âˆƒ v, loc â†¦ v) -âˆ—
     WP lock_client #loc lock {{ _, True }}.
@@ -535,6 +537,28 @@ Section lock.
     { iFrame "Hislock". eauto. }
     eauto.
   Qed.
-
 End lock.
+Section spin_lock.
+  Local Existing Instance spin_lock.
 
+  Definition spin_lock_client : val :=
+    Î»: "loc" "lock",
+      acquire "lock";;
+      "loc" <- #42;;
+      release "lock".
+
+  (* Making sure that using [spin_lockG] here works, not just [lockG]. *)
+  Context `{!heapGS Î£, !spin_lockG Î£}.
+
+  Lemma wp_spin_lock_client loc lock Î³ :
+    is_lock Î³ lock (âˆƒ v, loc â†¦ v) -âˆ—
+    WP spin_lock_client #loc lock {{ _, True }}.
+  Proof.
+    iIntros "#Hislock".
+    wp_lam. wp_smart_apply (acquire_spec with "Hislock") as "[Hlocked [%v Hloc]]".
+    wp_store.
+    wp_smart_apply (release_spec with "[$Hlocked Hloc]").
+    { iFrame "Hislock". eauto. }
+    eauto.
+  Qed.
+End spin_lock.
-- 
GitLab