Merge pull request #46 from mtzguido/lock_alive_inj

SpinLock: prove (a version of) the injectivity lemma
FStarLang · Apr 13, 2024 · 0ede0b7 · 0ede0b7
2 parents 3a5ed3e + 495ac54
commit 0ede0b7
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 0 deletions.
diff --git a/lib/pulse/lib/Pulse.Lib.SpinLock.fst b/lib/pulse/lib/Pulse.Lib.SpinLock.fst
@@ -231,3 +231,27 @@ fn free_aux (#v:vprop) (l:lock)
 ```
 
 let free = free_aux
+
+```pulse
+ghost
+fn __lock_alive_inj
+  (l:lock) (#p1 #p2 :perm) (#v1 #v2 :vprop)
+  requires lock_alive l #p1 v1 ** lock_alive l #p2 v2
+  ensures  lock_alive l #p1 v1 ** lock_alive l #p2 v1
+{
+  unfold (lock_alive l #p1 v1);
+  unfold (lock_alive l #p2 v2);
+  invariant_name_identifies_invariant
+    (iref_of l.i) (iref_of l.i);
+  assert (
+    pure (
+      cinv_vp l.i (lock_inv l.r l.gr v1)
+      ==
+      cinv_vp l.i (lock_inv l.r l.gr v2)
+    )
+  );
+  fold (lock_alive l #p1 v1);
+  fold (lock_alive l #p2 v1);
+}
+```
+let lock_alive_inj = __lock_alive_inj
diff --git a/lib/pulse/lib/Pulse.Lib.SpinLock.fsti b/lib/pulse/lib/Pulse.Lib.SpinLock.fsti
@@ -51,3 +51,10 @@ val gather2 (#v:vprop) (#p : perm) (l:lock)
 
 val free (#v:vprop) (l:lock)
   : stt unit (lock_alive l #full_perm v ** lock_acquired l) (fun _ -> emp)
+
+(* A given lock is associated to a single vprop, roughly.
+I'm not sure if we can prove v1 == v2 here. *)
+val lock_alive_inj (l:lock) (#p1 #p2 : perm) (#v1 #v2 : vprop)
+  : stt_ghost unit emp_inames
+              (lock_alive l #p1 v1 ** lock_alive l #p2 v2)
+              (fun _ -> lock_alive l #p1 v1 ** lock_alive l #p2 v1)