wip

Author: gebner

lib/common/Pulse.Lib.Core.fsti

@@ -450,7 +450,7 @@ inline_for_extraction instance non_informative_loc_id
   : NonInformative.non_informative loc_id
   = { reveal = (fun x -> reveal x) <: NonInformative.revealer loc_id }
 
-val loc : loc_id -> slprop
+val loc : loc_id -> timeless_slprop
 
 val loc_get () : stt_ghost loc_id emp_inames emp (fun l -> loc l)
 val loc_dup l : stt_ghost unit emp_inames (loc l) (fun _ -> loc l ** loc l)
@@ -460,6 +460,12 @@ val on (l:loc_id) ([@@@mkey] p:slprop) : slprop
 val on_intro #l p : stt_ghost unit emp_inames (loc l ** p) (fun _ -> loc l ** on l p)
 val on_elim #l p : stt_ghost unit emp_inames (loc l ** on l p) (fun _ -> loc l ** p)
 
+val timeless_on (l:loc_id) (p : slprop)
+: Lemma
+    (requires timeless p)
+    (ensures timeless (on l p))
+    [SMTPat (timeless (on l p))]
+
 [@@Tactics.Typeclasses.tcclass; erasable]
 type placeless (p: slprop) =
   l:loc_id -> l':loc_id -> stt_ghost unit emp_inames (on l p) (fun _ -> on l' p)
@@ -510,6 +516,9 @@ val later_star p q : squash (later (p ** q) == later p ** later q)
 val later_exists (#t: Type) (f:t->slprop) : stt_ghost unit emp_inames (later (exists* x. f x)) (fun _ -> exists* x. later (f x))
 val exists_later (#t: Type) (f:t->slprop) : stt_ghost unit emp_inames (exists* x. later (f x)) (fun _ -> later (exists* x. f x))
 
+val later_on l p : stt_ghost unit emp_inames (later (on l p)) (fun _ -> on l (later p))
+val on_later l p : stt_ghost unit emp_inames (on l (later p)) (fun _ -> later (on l p))
+
 //////////////////////////////////////////////////////////////////////////
 // Equivalence
 //////////////////////////////////////////////////////////////////////////

lib/core/Pulse.Lib.Core.fst

@@ -196,6 +196,8 @@ let on l p = p
 let on_intro p = admit ()
 let on_elim p = admit ()
 
+let timeless_on = admit ()
+
 let placeless_emp = admit ()
 let placeless_star _ _ = admit ()
 let placeless_pure _ = admit ()
@@ -241,6 +243,9 @@ let exists_later #t f =
   let h: squash ((exists* x. later (f x)) `implies` later (exists* x. f x)) = h in
   A.implies_elim _ _
 
+let later_on = admit ()
+let on_later = admit ()
+
 //////////////////////////////////////////////////////////////////////////
 // Equivalence
 //////////////////////////////////////////////////////////////////////////

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

@@ -28,7 +28,7 @@ ghost fn placeless_inv i p {| inst: placeless p |} : placeless (inv i p) = l1 l2
     loc_gather l1 #l_;
     drop_ (move_tag l_ l' p _ _);
     ghost_impersonate l2 (C.inv i (on l' p)) (on l2 (inv i p)) fn _ {
-      fold move_tag l2 l' p (aux inst l2 l') (aux inst l' l2);
+      fold move_tag l2 l' p (aux #p inst l2 l') (aux #p inst l' l2);
       loc_dup l2;
       fold inv i p;
       on_intro (inv i p);
@@ -76,3 +76,27 @@ ghost fn dup_inv i p () : duplicable_f (inv i p) = {
 
 instance duplicable_inv i p : duplicable (inv i p) =
   { dup_f = dup_inv i p }
+
+open PulseCore.Observability
+
+unobservable fn with_inv_unobs u#a (#a: Type u#a) #is (i: iname { not (mem_inv is i) }) (p: slprop) pre (post: a->slprop)
+    (k: unit -> stt_atomic a #Neutral is (pre ** later p) (fun x -> post x ** later p))
+  opens is
+  preserves inv i p
+  requires pre
+  returns x:a
+  ensures post x
+{
+  unfold inv i p; with l_ l' f g. _;
+  assume pure (inames_subset (add_inv is i) is);
+  let x = with_invariant #a #Neutral #pre #post #is #(on l' p) i fn _ {
+    later_on l' p;
+    // { let g=g; g() };
+    admit ();
+    let x = k ();
+    on_later l' p;
+    x
+  };
+  admit ();
+  fold inv i p;
+}

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

@@ -21,10 +21,6 @@ module U32 = FStar.UInt32
 module OR = Pulse.Lib.OnRange
 module SLT = Pulse.Lib.SLPropTable
 module Box = Pulse.Lib.Box
-  
-instance assume_box_is_atomic (r: Box.box U32.t) p i :
-    is_send (pts_to r #p i) =
-  admit ()
 
 noeq
 type cvar_t_core = {
@@ -97,6 +93,8 @@ let cvar_inv (b: cvar_t_core) (p:slprop)
     pure (Seq.length preds == n) **
     maybe_holds v p preds
 
+instance is_send_cvar_inv b p : is_send (cvar_inv b p) = admit ()
+
 let cvar (b: cvar_t) (p:slprop)
 : slprop
 = exists* l'. in_same_process l' **
@@ -171,7 +169,6 @@ ensures
   ensures later (on l <| cvar_inv b.core p)
   {
      later_elim _;
-     admit ();
      is_send_elim_on (cvar_inv b.core p) #_;
      unfold cvar_inv;
      Box.gather b.core.r;
@@ -185,7 +182,9 @@ ensures
      rewrite (istar preds) as (maybe_holds 1ul p preds);
      Box.share b.core.r;
      fold (cvar_inv b.core p);
-     later_intro (cvar_inv b.core p);
+     is_send_intro_on (cvar_inv b.core p) l;
+     later_intro (on l <| cvar_inv b.core p);
+     drop_ (in_same_process l);
      drop_ (Box.pts_to b.core.r #0.5R _)
   };
   drop_ (inv _ _)
@@ -267,13 +266,14 @@ ensures
             (if res then p else SLT.pts_to b.core.tab i #0.5R p)
     {
       later_elim _;
-      admit ();
+      is_send_elim_on (cvar_inv b.core q) #_;
       unfold cvar_inv;
       let vv = read_atomic_box b.core.r;
       if (vv = 0ul)
       {
         fold (cvar_inv b.core q);
-        later_intro (cvar_inv b.core q);
+        is_send_intro_on (cvar_inv b.core q) l;
+        later_intro (on l <| cvar_inv b.core q);
         drop_ (later_credit 1);
         false;
       }
@@ -306,7 +306,8 @@ ensures
         rewrite (istar preds') as (maybe_holds v q preds');
         // fold (maybe_holds v q preds');
         fold (cvar_inv b.core q);
-        later_intro (cvar_inv b.core q);
+        is_send_intro_on (cvar_inv b.core q) l;
+        later_intro (on l <| cvar_inv b.core q);
         drop_ (SLT.pts_to b.core.tab i #0.5R _);
         true
       }
@@ -448,7 +449,7 @@ opens
         SLT.pts_to b.core.tab k #0.5R p2)
     {
       later_elim _;
-      admit ();
+      is_send_elim_on (cvar_inv b.core q) #_;
       unfold cvar_inv;
       with v preds. assert (maybe_holds v q preds);
       get_predicate_at_i b.core.tab i (p1 ** p2) preds;
@@ -482,7 +483,8 @@ opens
         // step ();
         rewrite equiv (istar preds') q as maybe_holds v q preds';
         fold (cvar_inv b.core q);
-        later_intro (cvar_inv b.core q);
+        is_send_intro_on (cvar_inv b.core q) l;
+        later_intro (on l <| cvar_inv b.core q);
         drop_ (SLT.pts_to b.core.tab i #0.5R emp);
       }
       else
@@ -491,7 +493,8 @@ opens
         rewrite_istar preds preds' i p1 p2 q;
         rewrite istar preds' as maybe_holds v q preds';
         fold (cvar_inv b.core q);
-        later_intro (cvar_inv b.core q);
+        is_send_intro_on (cvar_inv b.core q) l;
+        later_intro (on l <| cvar_inv b.core q);
         drop_ (SLT.pts_to b.core.tab i #0.5R emp);
       }
     };

lib/pulse/lib/Pulse.Lib.SpinLock.fst

@@ -24,10 +24,6 @@ module U32 = FStar.UInt32
 module B = Pulse.Lib.Box
 module GR = Pulse.Lib.GhostReference
 module CInv = Pulse.Lib.CancellableInvariant
-  
-instance assume_box_is_atomic (r: B.box U32.t) i :
-    is_send (pts_to r #1.0R i) =
-  admit ()
 
 let lock_inv_aux l' (r:B.box U32.t) (gr:GR.ref U32.t) (v:slprop) : slprop  =
   exists* i p. pts_to r #1.0R i **
@@ -37,7 +33,7 @@ let lock_inv_aux l' (r:B.box U32.t) (gr:GR.ref U32.t) (v:slprop) : slprop  =
                      (i =!= 0ul ==> p == 0.5R)) 
 
 let is_send_if (i: U32.t) (v: slprop) (inst: is_send v) : is_send (if i = 0ul then v else emp) =
-  if i = 0ul then inst else is_send_placeless emp #placeless_emp
+  if i = 0ul then inst else is_send_placeless emp
 
 instance is_send_lock_inv_aux l' r gr v : is_send (lock_inv_aux l' r gr v) =
   Tactics.Typeclasses.solve

lib/pulse/lib/pledge/Pulse.Lib.SendableTrade.fst

@@ -27,7 +27,18 @@ let trade (#is:inames) (hyp concl:slprop) =
   exists* extra inst f. extra ** trade_elim_exists is hyp extra concl inst f
 
 ghost fn is_send_trade #is (p1 p2: slprop) : is_send (trade #is p1 p2) = l l' {
-  admit ()
+  ghost_impersonate l (on l (trade #is p1 p2)) (on l' (trade #is p1 p2)) fn _ {
+    on_elim (trade #is p1 p2);
+    unfold trade #is p1 p2; with extra inst f. _;
+    on_intro extra;
+    is_send_elim extra #inst l';
+    ghost_impersonate l' (on l' extra ** trade_elim_exists is p1 extra p2 inst f)
+        (on l' (trade #is p1 p2)) fn _ {
+      on_elim extra;
+      fold trade #is p1 p2;
+      on_intro (trade #is p1 p2);
+    }
+  }
 }
 
 ghost