diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 114ce325ec24db5c5b02efefc322c559cc7e6778..613d78114412de1c14359c7d228eb37c33171eed 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -304,18 +304,3 @@ goal 2 is:
The command has indeed failed with message:
Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in
(#() #()).
-"wp_spin_lock_client"
- : string
-1 goal
-
- Σ : gFunctors
- heapGS0 : heapGS Σ
- spin_lockG0 : spin_lockG Σ
- loc : locations.loc
- lock : val
- γ : lock_name
- ============================
- "Hislock" : is_lock γ lock (∃ v : val, loc ↦ v)
- --------------------------------------â–¡
- WP let: "lock" := lock in acquire "lock";; #loc <- #42;; release "lock"
- {{ _, True }}
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index eb741db312fa4ba9102c7428032d5be3ffe76e6c..00f88936305c3f1a08cc7d91557fac7c890e1e5c 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,8 +1,9 @@
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.spin_lock.
+From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation.
From iris.prelude Require Import options.
+(* For printing tests we want stable names. *)
Unset Mangle Names.
Section tests.
@@ -513,53 +514,3 @@ Proof.
iIntros (?) "_". rewrite /heap_e /=.
wp_alloc l. wp_load. wp_store. wp_load. auto.
Qed.
-
-(** Just making sure the lock typeclass actually works. *)
-Section lock.
- Context `{!lock}.
-
- Definition lock_client : val :=
- λ: "loc" "lock",
- acquire "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 }}.
- 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 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 Σ}.
-
- Check "wp_spin_lock_client".
- 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. simpl. Show.
- 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.
diff --git a/tests/lock.ref b/tests/lock.ref
new file mode 100644
index 0000000000000000000000000000000000000000..1e518c193755fbdc09e38bdae1049643db3e6546
--- /dev/null
+++ b/tests/lock.ref
@@ -0,0 +1,12 @@
+"wp_lock_client_spin"
+ : string
+1 goal
+
+ Σ : gFunctors
+ heapGS0 : heapGS Σ
+ spin_lockG0 : spin_lockG Σ
+ ============================
+ ⊢ WP let: "l" := ref #10 in
+ let: "lock" := newlock #() in
+ acquire "lock";; "l" <- #42;; release "lock"
+ {{ _, True }}
diff --git a/tests/lock.v b/tests/lock.v
new file mode 100644
index 0000000000000000000000000000000000000000..fda5baa55890a681dbf4e400da5b0927041e4024
--- /dev/null
+++ b/tests/lock.v
@@ -0,0 +1,82 @@
+From iris.heap_lang Require Import proofmode notation adequacy lib.spin_lock.
+From iris.prelude Require Import options.
+
+(* For printing tests we want stable names. *)
+Unset Mangle Names.
+
+(** Make sure the lock type class works to write generic clients and
+specifications. *)
+Section lock_gen.
+ Context `{!lock}.
+
+ Definition lock_client_gen : expr :=
+ let: "l" := ref #10 in
+ let: "lock" := newlock #() in
+ acquire "lock";;
+ "l" <- #42;;
+ release "lock".
+
+ Lemma wp_lock_client_gen `{!heapGS Σ, !lockG Σ} :
+ ⊢ WP lock_client_gen {{ _, True }}.
+ Proof.
+ unfold lock_client_gen. wp_alloc l as "Hl".
+ wp_smart_apply (newlock_spec (∃ n : Z, l ↦ #n) with "[Hl]")
+ as (lk γ) "#Hlock"; first by eauto.
+ wp_smart_apply (acquire_spec with "Hlock") as "(Hlocked & %v & Hloc)".
+ wp_store.
+ wp_smart_apply (release_spec with "[$Hlock $Hlocked Hloc]"); by eauto.
+ Qed.
+End lock_gen.
+
+(** Make sure the lock type class works to write clients and
+specifications for specific locks (here: spin lock). *)
+Section lock_spin.
+ Local Existing Instance spin_lock.
+
+ Definition lock_client_spin : expr :=
+ let: "l" := ref #10 in
+ let: "lock" := newlock #() in
+ acquire "lock";;
+ "l" <- #42;;
+ release "lock".
+
+ (* Making sure that using [spin_lockG] here works, not just [lockG]. *)
+ Check "wp_lock_client_spin".
+ Lemma wp_lock_client_spin `{!heapGS Σ, !spin_lockG Σ} :
+ ⊢ WP lock_client_spin {{ _, True }}.
+ Proof.
+ unfold lock_client_spin.
+ (* This should not unfold the [newlock], [acquire], and [release]
+ projections. That is, it should not show [spin_lock.<something>]. *)
+ simpl. Show.
+ wp_alloc l as "Hl".
+ wp_smart_apply (newlock_spec (∃ n : Z, l ↦ #n) with "[Hl]")
+ as (lk γ) "#Hlock"; first by eauto.
+ wp_smart_apply (acquire_spec with "Hlock") as "(Hlocked & %v & Hloc)".
+ wp_store.
+ wp_smart_apply (release_spec with "[$Hlock $Hlocked Hloc]"); by eauto.
+ Qed.
+End lock_spin.
+
+(** Making sure that the [lockG/spin_lockG] conditions are resolved when using adequacy. For
+the generic client, we need to instantiate it with a specific lock for that to
+make sense. *)
+Section lock_adequacy.
+ Local Existing Instance spin_lock.
+
+ Lemma lock_client_gen_adequate σ :
+ adequate NotStuck lock_client_gen σ (λ _ _, True).
+ Proof.
+ set (Σ := #[heapΣ; spin_lockΣ]).
+ apply (heap_adequacy Σ); iIntros (?) "_".
+ iApply wp_lock_client_gen.
+ Qed.
+
+ Lemma lock_client_spin_adequate σ :
+ adequate NotStuck lock_client_spin σ (λ _ _, True).
+ Proof.
+ set (Σ := #[heapΣ; spin_lockΣ]).
+ apply (heap_adequacy Σ); iIntros (?) "_".
+ iApply wp_lock_client_gen.
+ Qed.
+End lock_adequacy.