make sure the interface predicates are not accidentally unfolded

iris_heap_lang/lib/atomic_heap.v

@@ -74,6 +74,13 @@ Class atomic_heap := AtomicHeap {
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
 
+Global Arguments alloc : simpl never.
+Global Arguments free : simpl never.
+Global Arguments load : simpl never.
+Global Arguments store : simpl never.
+Global Arguments cmpxchg : simpl never.
+Global Arguments mapsto : simpl never.
+
 Existing Class atomic_heapGS.
 Global Hint Mode atomic_heapGS + + : typeclass_instances.
 Global Hint Extern 0 (atomic_heapGS _) => progress simpl : typeclass_instances.

iris_heap_lang/lib/lock.v

@@ -49,6 +49,12 @@ Class lock := Lock {
     {{{ is_lock (L:=L) γ lk R ∗ locked (L:=L) γ ∗ R }}} release lk {{{ RET #(); True }}}
 }.
 
+Global Arguments newlock : simpl never.
+Global Arguments acquire : simpl never.
+Global Arguments release : simpl never.
+Global Arguments is_lock : simpl never.
+Global Arguments locked : simpl never.
+
 Existing Class lockG.
 Global Hint Mode lockG + + : typeclass_instances.
 Global Hint Extern 0 (lockG _) => progress simpl : typeclass_instances.

iris_heap_lang/lib/rw_lock.v

@@ -72,6 +72,15 @@ Class rwlock := RwLock {
     {{{ RET #(); True }}};
 }.
 
+Global Arguments newlock : simpl never.
+Global Arguments acquire_reader : simpl never.
+Global Arguments release_reader : simpl never.
+Global Arguments acquire_writer : simpl never.
+Global Arguments release_writer : simpl never.
+Global Arguments is_rw_lock : simpl never.
+Global Arguments reader_locked : simpl never.
+Global Arguments writer_locked : simpl never.
+
 Existing Class rwlockG.
 Global Hint Mode rwlockG + + : typeclass_instances.
 Global Hint Extern 0 (rwlockG _) => progress simpl : typeclass_instances.

tests/heap_lang.ref

@@ -304,3 +304,18 @@ 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

@@ -550,12 +550,13 @@ Section spin_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. wp_smart_apply (acquire_spec with "Hislock") as "[Hlocked [%v Hloc]]".
+    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. }