removing ghost_witness/ghost_recall

FStarLang · Feb 29, 2024 · 4e73180 · 4e73180
1 parent 8631125
commit 4e73180
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 57 deletions.
diff --git a/lib/pulse/core/PulseCore.Atomic.fst b/lib/pulse/core/PulseCore.Atomic.fst
@@ -302,30 +302,4 @@ let ghost_read
 let ghost_write r x y f = Ghost.hide (A.ghost_write r x y f)
 let ghost_share r v0 v1 = Ghost.hide (A.ghost_share r v0 v1)
 let ghost_gather r v0 v1 = Ghost.hide (A.ghost_gather r v0 v1) 
-
-let ghost_witnessed 
-    (#a:Type u#1) 
-    (#p:pcm a)
-    (r:ghost_ref p)
-    (f:property a)
-= admit() //witnessed (reveal r) f
-
-let ghost_witness
-    (#a:Type)
-    (#pcm:pcm a)
-    (r:ghost_ref pcm)
-    (fact:stable_property pcm)
-    (v:Ghost.erased a)
-    (pf:squash (forall z. compatible pcm v z ==> fact z))
-= admit() //A.witness r fact v pf
-
-let ghost_recall
-    (#a:Type u#1)
-    (#pcm:pcm a)
-    (#fact:property a)
-    (r:ghost_ref pcm)
-    (v:Ghost.erased a)
-    (w:ghost_witnessed r fact)
-= admit() //A.recall r v w
-
 let drop p = Ghost.hide (A.drop p)
diff --git a/lib/pulse/core/PulseCore.Atomic.fsti b/lib/pulse/core/PulseCore.Atomic.fsti
@@ -401,37 +401,39 @@ val ghost_gather
     (ghost_pts_to r v0 ** ghost_pts_to r v1)
     (fun _ -> ghost_pts_to r (op pcm v0 v1))
 
-val ghost_witnessed
-    (#a:Type u#1)
-    (#p:pcm a)
-    (r:ghost_ref p)
-    (f:property a)
-: Type0
-
-val ghost_witness
-    (#a:Type)
-    (#pcm:pcm a)
-    (r:ghost_ref pcm)
-    (fact:stable_property pcm)
-    (v:Ghost.erased a)
-    (pf:squash (forall z. compatible pcm v z ==> fact z))
-: stt_atomic
-    (ghost_witnessed r fact)
-    #Unobservable emp_inames
-    (ghost_pts_to r v)
-    (fun _ -> ghost_pts_to r v)
-
-val ghost_recall
-    (#a:Type u#1)
-    (#pcm:pcm a)
-    (#fact:property a)
-    (r:ghost_ref pcm)
-    (v:Ghost.erased a)
-    (w:ghost_witnessed r fact)
-: stt_atomic (v1:Ghost.erased a{compatible pcm v v1})
-    #Unobservable emp_inames
-    (ghost_pts_to r v)
-    (fun v1 -> ghost_pts_to r v ** pure (fact v1))
+// Unused?
+
+// val ghost_witnessed
+//     (#a:Type u#1)
+//     (#p:pcm a)
+//     (r:ghost_ref p)
+//     (f:property a)
+// : Type0
+
+// val ghost_witness
+//     (#a:Type)
+//     (#pcm:pcm a)
+//     (r:ghost_ref pcm)
+//     (fact:stable_property pcm)
+//     (v:Ghost.erased a)
+//     (pf:squash (forall z. compatible pcm v z ==> fact z))
+// : stt_atomic
+//     (ghost_witnessed r fact)
+//     #Unobservable emp_inames
+//     (ghost_pts_to r v)
+//     (fun _ -> ghost_pts_to r v)
+
+// val ghost_recall
+//     (#a:Type u#1)
+//     (#pcm:pcm a)
+//     (#fact:property a)
+//     (r:ghost_ref pcm)
+//     (v:Ghost.erased a)
+//     (w:ghost_witnessed r fact)
+// : stt_atomic (v1:Ghost.erased a{compatible pcm v v1})
+//     #Unobservable emp_inames
+//     (ghost_pts_to r v)
+//     (fun v1 -> ghost_pts_to r v ** pure (fact v1))
 
 val drop (p:slprop)
 : stt_ghost unit p (fun _ -> emp)