From fc4b08fe0f080edb9c8840ff96c2f3c86d373528 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 Aug 2022 17:32:20 +0000
Subject: [PATCH] logatom_lock tweaks

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

diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 3fd5d26ff..61dc2888e 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -1,6 +1,7 @@
 (** A TaDA-style logically atomic specification for a lock, derived for an
     arbitrary implementation of the lock interfacne. The opposite direction
-    could also be derived rather easily, as shown in the TaDA paper.
+    could also be derived rather easily (modulo a later in the [acquire] postcondition
+    or a restriction to timeless lock invariants), as shown in the TaDA paper.
 
     In essence, this is an instance of the general fact that 'invariant-based'
     ("HoCAP-style") logically atomic specifications are equivalent to TaDA-style
@@ -27,8 +28,8 @@ Section tada.
   Context `{!heapGS Σ, !lockG Σ} (l : lock).
 
   Record tada_lock_name := TadaLockName {
-      tada_lock_name_state : gname;
-      tada_lock_name_lock : l.(name);
+    tada_lock_name_state : gname;
+    tada_lock_name_lock : l.(name);
   }.
   
   Definition tada_lock_state (γ : tada_lock_name) (s : state) : iProp Σ :=
-- 
GitLab