From af0a091bbea82ce3ede8305eee450c3032b85dd5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Aug 2023 16:38:57 +0200
Subject: [PATCH] make sure the interface predicates are not accidentally
 unfolded

---
 iris_heap_lang/lib/atomic_heap.v |  7 +++++++
 iris_heap_lang/lib/lock.v        |  6 ++++++
 iris_heap_lang/lib/rw_lock.v     |  9 +++++++++
 tests/heap_lang.ref              | 15 +++++++++++++++
 tests/heap_lang.v                |  5 +++--
 5 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 5d1b84822..b356f550a 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/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.
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index a7ba1b213..b06b4f1cb 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/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.
diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index d42ed7c52..57060fd98 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/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.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 613d78114..114ce325e 100644
--- a/tests/heap_lang.ref
+++ b/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 }}
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index c5f966bb0..eb741db31 100644
--- a/tests/heap_lang.v
+++ b/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. }
-- 
GitLab