Merge branch 'ralf/locktest' into 'master'

Test that lock `Σ`s can be found in adequacy

See merge request iris/iris!981

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 }}

tests/heap_lang.v

 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.

tests/lock.ref

+"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 }}

tests/lock.v

+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.