wip

Author: gebner

lib/pulse/lib/Pulse.Lib.Reference.fst

@@ -38,11 +38,6 @@ let pts_to (#a: Type u#a) (r:ref a) (#[T.exact (`1.0R)] p:perm) (n:a)
 = A.pts_to r #p (singleton n)
 let is_send_pts_to r n = Tactics.Typeclasses.solve
 
-let atomic_loc = admit ()
-let elim_atomic_loc = admit ()
-let unsafe_attest_atomic_acquired = admit ()
-let unsafe_attest_atomic_released = admit ()
-
 let pts_to_timeless _ _ _ = ()
 
 let is_full_ref = A.is_full_array

lib/pulse/lib/Pulse.Lib.Reference.fsti

@@ -35,24 +35,6 @@ val pts_to (#a:Type u#a) ([@@@mkey]r:ref a) (#[T.exact (`1.0R)] p:perm) (n:a) :
 
 instance val is_send_pts_to #a r #p n : is_send (pts_to #a r #p n)
 
-val atomic_loc #a (l: loc_id) (x: ref a) : l':loc_id { process_of l' == process_of l }
-
-ghost fn elim_atomic_loc u#a (#a: Type u#a) (l: loc_id) (x: ref a) (p: slprop)
-  requires on (atomic_loc l x) p
-  ensures on (process_of l) p
-
-[@@deprecated "UNSAFE"]
-ghost fn unsafe_attest_atomic_released u#a (#a: Type u#a) (p: slprop) {| is_send p |} (#l:loc_id) (x: ref a)
-  preserves loc l
-  requires p
-  requires on (atomic_loc l x) p
-
-[@@deprecated "UNSAFE"]
-ghost fn unsafe_attest_atomic_acquired u#a (#a: Type u#a) (p: slprop) {| is_send p |} (#l:loc_id) (x: ref a)
-  preserves loc l
-  requires on (atomic_loc l x) p
-  ensures p
-
 [@@pulse_unfold]
 instance has_pts_to_ref (a:Type u#a) : has_pts_to (ref a) a = {
   pts_to = (fun r #f v -> pts_to r #f v);