From fd02cdaa69fcff6b942bd6c491944a3d38ef984c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Feb 2023 17:53:20 +0100
Subject: [PATCH] In logatom lock: Formalize that the lock is Free before
 acquire.

---
 iris_heap_lang/lib/logatom_lock.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index d9556ceb3..4b3912b05 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -74,7 +74,7 @@ Section tada.
     tada_is_lock γ lk -∗
     <<< ∀∀ s, tada_lock_state γ s >>>
       l.(acquire) lk @ ∅
-    <<< tada_lock_state γ Locked, RET #() >>>.
+    <<< ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked, RET #() >>>.
   Proof.
     iIntros "#Hislock %Φ AU". iApply wp_fupd.
     wp_apply (l.(acquire_spec) with "Hislock").
@@ -83,7 +83,7 @@ Section tada.
     iDestruct (ghost_var_agree with "Hvar1 Hvar2") as %<-.
     iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
     { rewrite Qp.quarter_three_quarter //. }
-    iMod ("Hclose" with "[$Hvar2 $Hlocked $Hvar1]"). done.
+    iMod ("Hclose" with "[$Hvar2 $Hlocked $Hvar1]"); done.
   Qed.
 
   Lemma release_tada_spec γ lk :
-- 
GitLab