wip

Author: gebner

lib/pulse/lib/Pulse.Lib.BetterInv.fst

@@ -36,7 +36,7 @@ ghost fn placeless_inv i p {| inst: placeless p |} : placeless (inv i p) = l1 l2
   }
 }
 
-ghost fn is_sync_inv i p {| is_sync p |} : is_sync (inv i p) = l1 l2 {
+ghost fn is_send_inv i p {| is_send p |} : is_send (inv i p) = l1 l2 {
   ghost_impersonate l1 (on l1 (inv i p)) (on l2 (inv i p)) fn _ {
     on_elim (inv i p);
     unfold inv i p; with l_ l' f g. _;
@@ -47,15 +47,15 @@ ghost fn is_sync_inv i p {| is_sync p |} : is_sync (inv i p) = l1 l2 {
         requires on l2 p
         ensures on l' p
       {
-        is_sync_elim p l1;
+        is_send_elim p l1;
         let f = f; f ()
       };
       ghost fn g' ()
         requires on l' p
         ensures on l2 p
       {
         let g = g; g ();
-        is_sync_elim p l2;
+        is_send_elim p l2;
       };
       fold move_tag l2 l' p f' g';
       loc_dup l2;

lib/pulse/lib/Pulse.Lib.BetterInv.fsti

@@ -7,5 +7,5 @@ open Pulse.Class.Duplicable
 val inv (i: iname) (p: slprop) : slprop
 
 instance val placeless_inv i p {| placeless p |} : placeless (inv i p)
-instance val is_sync_inv i p {| is_sync p |} : is_sync (inv i p)
+instance val is_send_inv i p {| is_send p |} : is_send (inv i p)
 instance val duplicable_inv i p : duplicable (inv i p)

lib/pulse/lib/Pulse.Lib.ConditionVar.fst

@@ -23,7 +23,7 @@ module SLT = Pulse.Lib.SLPropTable
 module Box = Pulse.Lib.Box
 
 instance assume_box_is_atomic (r: Box.box U32.t) p i :
-    is_sync (pts_to r #p i) =
+    is_send (pts_to r #p i) =
   admit ()
 
 noeq
@@ -115,8 +115,8 @@ let recv (b: cvar_t) (p:slprop)
     cvar b q **
     SLT.pts_to b.core.tab i #0.5R p
 
-instance is_sync_send c p : is_sync (send c p) = Tactics.Typeclasses.solve
-instance is_sync_recv c p : is_sync (recv c p) = Tactics.Typeclasses.solve
+instance is_send_send c p : is_send (send c p) = Tactics.Typeclasses.solve
+instance is_send_recv c p : is_send (recv c p) = Tactics.Typeclasses.solve
 
 fn create (p:slprop)
   requires emp
@@ -172,7 +172,7 @@ ensures
   {
      later_elim _;
      admit ();
-     is_sync_elim_on (cvar_inv b.core p) #_;
+     is_send_elim_on (cvar_inv b.core p) #_;
      unfold cvar_inv;
      Box.gather b.core.r;
      with v preds. assert (maybe_holds v p preds);

lib/pulse/lib/Pulse.Lib.ConditionVar.fsti

@@ -27,8 +27,8 @@ val send (c:cvar_t) (p:slprop) : slprop
 
 val recv (c:cvar_t) (p:slprop) : slprop
 
-instance val is_sync_send c p : is_sync (send c p)
-instance val is_sync_recv c p : is_sync (recv c p)
+instance val is_send_send c p : is_send (send c p)
+instance val is_send_recv c p : is_send (recv c p)
 
 fn create (p:slprop)
   requires emp

lib/pulse/lib/Pulse.Lib.Mutex.fst

@@ -40,7 +40,7 @@ let lock_inv (#a:Type0) (r:B.box a) (v:a -> slprop) : slprop =
 
 let mutex_live #a m #p v = lock_alive m.l #p (lock_inv m.r v)
 
-let is_sync_mutex_live #a m #p v = Tactics.Typeclasses.solve
+let is_send_mutex_live #a m #p v = Tactics.Typeclasses.solve
 
 let pts_to mg #p x = pts_to mg #p x
 

lib/pulse/lib/Pulse.Lib.Mutex.fsti

@@ -36,7 +36,7 @@ val mutex_live
   (#[T.exact (`1.0R)] p:perm)
   (v:a -> slprop)  : slprop
 
-instance val is_sync_mutex_live #a m #p v : is_sync (mutex_live #a m #p v)
+instance val is_send_mutex_live #a m #p v : is_send (mutex_live #a m #p v)
 
 //
 // mutex_guard is a ref-like type

lib/pulse/lib/Pulse.Lib.SendSync.fst

@@ -14,147 +14,6 @@ ghost fn dup_in_same_process p () : duplicable_f (in_same_process p) = {
 instance duplicable_in_same_process p : duplicable (in_same_process p) =
   { dup_f = dup_in_same_process p }
 
-let can_see_writes_from (other_loc: loc_id) : slprop =
-  in_same_process other_loc **
-    emp // extra assumptions
-
-ghost fn can_see_writes_from_prop other_loc
-  preserves can_see_writes_from other_loc
-  ensures in_same_process other_loc
-{
-  unfold can_see_writes_from other_loc;
-  dup (in_same_process other_loc) ();
-  fold can_see_writes_from other_loc;
-}
-
-ghost fn writes_visible_in_prop other_loc
-  preserves writes_visible_in other_loc
-  ensures in_same_process other_loc
-{
-  unfold writes_visible_in other_loc;
-  with l. assert loc l; loc_dup l;
-  ghost_impersonate other_loc
-    (on other_loc (can_see_writes_from l))
-    (on other_loc (can_see_writes_from l) ** pure (process_of other_loc == process_of l))
-    fn _ {
-      on_elim (can_see_writes_from l);
-      can_see_writes_from_prop l;
-      on_intro (can_see_writes_from l);
-      unfold in_same_process l;
-      loc_gather other_loc #_;
-    };
-  fold in_same_process other_loc;
-  fold writes_visible_in other_loc;
-}
-
-
-[@@deprecated "UNSAFE"]
-ghost fn unsafe_attest_can_see_writes_from (other_loc: loc_id)
-    pre post (k: unit -> stt_ghost unit emp_inames (can_see_writes_from other_loc ** pre)
-      (fun _ -> can_see_writes_from other_loc ** post))
-  preserves in_same_process other_loc
-  requires pre
-  ensures post
-{
-  dup (in_same_process other_loc) ();
-  fold can_see_writes_from other_loc;
-  k ();
-  drop_ (can_see_writes_from other_loc);
-}
-
-[@@deprecated "UNSAFE"]
-ghost fn unsafe_attest_writes_visible_in (other_loc: loc_id)
-    pre post (k: unit -> stt_ghost unit emp_inames (writes_visible_in other_loc ** pre)
-      (fun _ -> writes_visible_in other_loc ** post))
-  preserves in_same_process other_loc
-  requires pre
-  ensures post
-{
-  unfold in_same_process other_loc;
-  with l. assert loc l;
-  on_intro pre;
-  ghost_impersonate other_loc (on l pre) (on l post) fn _ {
-    loc_dup other_loc;
-    fold in_same_process l;
-    unsafe_attest_can_see_writes_from l (loc other_loc ** on l pre) (loc other_loc ** on l post) fn _ {
-      on_intro (can_see_writes_from l);
-      ghost_impersonate l
-          (on other_loc (can_see_writes_from l) ** on l pre)
-          (on other_loc (can_see_writes_from l) ** on l post)
-          fn _ {
-        loc_dup l;
-        fold writes_visible_in other_loc;
-        on_elim pre;
-        k ();
-        on_intro post;
-        unfold writes_visible_in other_loc; with l'. _;
-        loc_gather l #l';
-        rewrite each l' as l;
-      };
-      on_elim (can_see_writes_from l);
-    };
-    drop_ (in_same_process l);
-  };
-  on_elim post;
-  fold in_same_process other_loc;
-}
-
-ghost fn is_send_acq (p: slprop) {| inst: is_send p |} (other_loc: loc_id)
-  preserves can_see_writes_from other_loc
-  requires on other_loc p
-  ensures p
-{
-  inst other_loc;
-}
-
-ghost fn is_send_rel (p: slprop) {| is_send p |} (other_loc: loc_id)
-  preserves writes_visible_in other_loc
-  requires p
-  ensures on other_loc p
-{
-  unfold writes_visible_in;
-  with l. assert loc l;
-  on_intro p;
-  ghost_impersonate other_loc
-    (on other_loc (can_see_writes_from l) ** on l p)
-    (on other_loc (can_see_writes_from l) ** on other_loc p)
-    fn _ {
-      on_elim (can_see_writes_from l);
-      is_send_acq p l;
-      on_intro p;
-      on_intro (can_see_writes_from l);
-    };
-  fold writes_visible_in other_loc;
-}
-
-[@@deprecated "UNSAFE"]
-ghost fn unsafe_attest_released (p: slprop) {| is_send p |} (#l:loc_id)
-  preserves loc l
-  requires p
-  ensures on (process_of l) p
-{
-  loc_dup l;
-  fold in_same_process (process_of l);
-  unsafe_attest_writes_visible_in (process_of l) p (on (process_of l) p)
-    fn _ { is_send_rel p (process_of l) };
-  unfold in_same_process (process_of l);
-  loc_gather l #_;
-}
-
-[@@deprecated "UNSAFE"]
-ghost fn unsafe_attest_acquired (p: slprop) {| is_send p |} (#l:loc_id)
-  preserves loc l
-  requires on (process_of l) p
-  ensures p
-{
-  loc_dup l;
-  fold in_same_process (process_of l);
-  unsafe_attest_can_see_writes_from (process_of l) (on (process_of l) p) p
-    fn _ { is_send_acq p (process_of l) };
-  unfold in_same_process (process_of l);
-  loc_gather l #_;
-}
-
 ghost fn on_star_elim #l (p q: slprop)
   requires on l (p ** q)
   ensures on l p
@@ -189,64 +48,65 @@ ghost fn on_exists_elim u#a #l (#a: Type u#a) (p: a -> slprop)
   }
 }
 
-ghost fn is_send_placeless p {| inst: placeless p |} : is_send p = l {
-  loc_get (); with l0. assert loc l0;
-  inst l l0;
-  on_elim p;
-  drop_ (loc l0);
-}
-
-ghost fn is_send_star p q {| is_send p, is_send q |} : is_send (p ** q) = l {
-  on_star_elim p q;
-  is_send_acq p l;
-  is_send_acq q l;
-}
-
-ghost fn is_send_exists' u#a (#a: Type u#a) (p: a->slprop) {| ((x:a) -> is_send (p x)) |} :
-    is_send (exists* x. p x) = l {
-  on_exists_elim p;
-  with x. assert on l (p x);
-  is_send_acq (p x) l;
-}
-let is_send_exists p = is_send_exists' p
-
-ghost fn is_sync_elim p {| inst: is_sync p |} #l l'
+ghost fn is_send_elim p {| inst: is_send p |} #l l'
   requires on l p
   requires pure (process_of l == process_of l')
   ensures on l' p
 {
   inst l l'
 }
 
-ghost fn is_sync_elim_on p {| is_sync p |} #l
+ghost fn is_send_elim_on p {| is_send p |} #l
   preserves in_same_process l
   requires on l p
   ensures p
 {
   unfold in_same_process l;
   with l0. assert loc l0;
-  is_sync_elim p l0;
+  is_send_elim p l0;
   on_elim p;
   fold in_same_process l;
 }
 
-ghost fn is_sync_intro_on p {| is_sync p |} l
+ghost fn is_send_intro_on p {| is_send p |} l
   preserves in_same_process l
   requires p
   ensures on l p
 {
   unfold in_same_process l;
   with l0. assert loc l0;
   on_intro p;
-  is_sync_elim p l;
+  is_send_elim p l;
   fold in_same_process l;
 }
 
-ghost fn is_sync_placeless p {| inst: placeless p |} : is_sync p = l l' {
+ghost fn is_send_elim_on' p {| is_send p |} #l
+  preserves loc l
+  requires on (process_of l) p
+  ensures p
+{
+  loc_dup l;
+  fold in_same_process (process_of l);
+  is_send_elim_on p #_;
+  drop_ (in_same_process (process_of l));
+}
+
+ghost fn is_send_intro_on' p {| is_send p |} l
+  preserves loc l
+  requires p
+  ensures on (process_of l) p
+{
+  loc_dup l;
+  fold in_same_process (process_of l);
+  is_send_intro_on p (process_of l);
+  drop_ (in_same_process (process_of l));
+}
+
+ghost fn is_send_placeless p {| inst: placeless p |} : is_send p = l l' {
   inst l l'
 }
 
-ghost fn is_sync_in_same_process p : is_sync (in_same_process p) = l l' {
+ghost fn is_send_in_same_process p : is_send (in_same_process p) = l l' {
   ghost_impersonate l
     (on l (in_same_process p))
     (on l' (in_same_process p))
@@ -262,35 +122,27 @@ ghost fn is_sync_in_same_process p : is_sync (in_same_process p) = l l' {
     }
 }
 
-ghost fn is_send_of_is_sync p {| is_sync p |} : is_send p = l {
-  can_see_writes_from_prop l;
-  unfold in_same_process l; with l0. assert loc l0;
-  is_sync_elim p l0;
-  on_elim p;
-  drop_ (loc l0);
-}
-
-ghost fn is_sync_star p q {| is_sync p, is_sync q |} : is_sync (p ** q) = l l' {
+ghost fn is_send_star p q {| is_send p, is_send q |} : is_send (p ** q) = l l' {
   on_star_elim p q;
-  is_sync_elim p l';
-  is_sync_elim q l';
+  is_send_elim p l';
+  is_send_elim q l';
   on_star_intro p q;
 }
 
-ghost fn is_sync_exists' u#a (#a: Type u#a) (p: a->slprop) {| ((x:a) -> is_sync (p x)) |} :
-    is_sync (exists* x. p x) = l l' {
+ghost fn is_send_exists' u#a (#a: Type u#a) (p: a->slprop) {| ((x:a) -> is_send (p x)) |} :
+    is_send (exists* x. p x) = l l' {
   ghost_impersonate l (on l (exists* x. p x)) (on l' (exists* x. p x)) fn _ {
     on_elim (exists* x. p x);
     with x. assert p x;
     on_intro (p x);
-    is_sync_elim (p x) l';
+    is_send_elim (p x) l';
     ghost_impersonate l' (on l' (p x)) (on l' (exists* x. p x)) fn _ {
       on_elim (p x);
       on_intro (exists* x. p x)
     };
   }
 }
-let is_sync_exists = is_sync_exists'
+let is_send_exists = is_send_exists'
 
 
 inline_for_extraction noextract fn fork'
@@ -299,11 +151,13 @@ inline_for_extraction noextract fn fork'
   requires pre
 {
   loc_get (); with l. assert loc l;
-  unsafe_attest_released pre #_ #l;
+  loc_dup l; fold in_same_process (process_of l);
+  is_send_intro_on pre (process_of l);
+  drop_ (in_same_process (process_of l));
   fork (on (process_of l) pre) #_ #l fn l' {
-    rewrite on (process_of l) pre as on (process_of l') pre;
-    unsafe_attest_acquired pre #_ #l';
-    drop_ (loc l');
+    fold in_same_process (process_of l);
+    is_send_elim_on pre #_;
+    drop_ (in_same_process (process_of l));
     f ();
   };
 }