wip

Author: gebner

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

@@ -21,22 +21,12 @@ let inv (i: iname) (p: slprop) =
 let aux #p (inst: placeless p) l1 l2 =
   fun () -> inst l1 l2
 
-ghost fn placeless_inv i p {| inst: placeless p |} : placeless (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'. _;
-    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 #p inst l2 l') (aux #p inst l' l2);
-      loc_dup l2;
-      fold inv i p;
-      on_intro (inv i p);
-    }
-  }
-}
-
-ghost fn is_send_inv i p {| is_send p |} : is_send (inv i p) = l1 l2 {
+ghost fn move i p l1 l2
+    (fwd: unit -> stt_ghost unit emp_inames (on l1 p) (fun _ -> on l2 p))
+    (bwd: unit -> stt_ghost unit emp_inames (on l2 p) (fun _ -> on l1 p))
+  requires on l1 (inv i p)
+  ensures on l2 (inv i p)
+{
   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 +37,15 @@ ghost fn is_send_inv i p {| is_send p |} : is_send (inv i p) = l1 l2 {
         requires on l2 p
         ensures on l' p
       {
-        is_send_elim p l1;
+        bwd ();
         let f = f; f ()
       };
       ghost fn g' ()
         requires on l' p
         ensures on l2 p
       {
         let g = g; g ();
-        is_send_elim p l2;
+        fwd ();
       };
       fold move_tag l2 l' p f' g';
       loc_dup l2;
@@ -65,6 +55,18 @@ ghost fn is_send_inv i p {| is_send p |} : is_send (inv i p) = l1 l2 {
   }
 }
 
+ghost fn placeless_inv i p {| inst: placeless p |} : placeless (inv i p) = l1 l2 {
+  move i p l1 l2
+    fn _ { inst l1 l2 }
+    fn _ { inst l2 l1 }
+}
+
+ghost fn is_send_inv i p {| is_send p |} : is_send (inv i p) = l1 l2 {
+  move i p l1 l2
+    fn _ { is_send_elim p l2 }
+    fn _ { is_send_elim p l1 }
+}
+
 ghost fn dup_inv i p () : duplicable_f (inv i p) = {
   unfold inv i p; with l l' f g. _;
   dup (C.inv i (on l' p)) ();
@@ -77,26 +79,85 @@ 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
+ghost fn new_invariant (p: slprop)
+  requires p
+  returns i: iname
+  ensures inv i p
+{
+  loc_get (); with l. assert loc l;
+  on_intro p;
+  let i = C.new_invariant (on l p) #_;
+  ghost fn f () requires on l p ensures on l p {};
+  fold move_tag l l p f f;
+  fold inv i p;
+  i
+}
+
+inline_for_extraction noextract
+ghost fn with_inv_g u#a (a: Type u#a)
+    is (i: iname { not (mem_inv is i) }) (p: slprop) pre (post: a->slprop)
+    (k: unit -> stt_ghost a is (pre ** p) (fun x -> post x ** p))
+  opens add_inv is i
+  preserves inv i p
+  requires later_credit 1
+  requires pre
+  returns x:a
+  ensures post x
+{
+  unfold inv i p; with l l' f g. _;
+  let x = with_invariant_g #a
+      #(pre ** later_credit 1 ** loc l)
+      #(fun x -> post x ** loc l) #is #(on l' p) i fn _ {
+    later_elim (on l' p);
+    { let g=g; g() };
+    on_elim p;
+    let x = k ();
+    on_intro p;
+    { let f=f; f() };
+    later_intro (on l' p);
+    x
+  };
+  fold inv i p;
+  x
+}
 
-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
+inline_for_extraction noextract
+atomic fn with_inv_atomic 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 #Observable is (pre ** p) (fun x -> post x ** p))
+  opens add_inv is i
   preserves inv i p
+  requires later_credit 1
   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 ();
+  unfold inv i p; with l l' f g. _;
+  let x = with_invariant #a #Observable
+      #(pre ** later_credit 1 ** loc l)
+      #(fun x -> post x ** loc l) #is #(on l' p) i fn _ {
+    later_elim (on l' p);
+    { let g=g; g() };
+    on_elim p;
     let x = k ();
-    on_later l' p;
+    on_intro p;
+    { let f=f; f() };
+    later_intro (on l' p);
     x
   };
-  admit ();
   fold inv i p;
+  x
+}
+
+inline_for_extraction noextract
+fn with_inv_stt 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 #Observable is (pre ** p) (fun x -> post x ** p))
+  preserves inv i p
+  requires pre
+  returns x:a
+  ensures post x
+{
+  later_credit_buy 1;
+  with_inv_atomic a is i p pre post k
 }

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

@@ -3,9 +3,52 @@ module Pulse.Lib.BetterInv
 open Pulse.Lib.Core
 open Pulse.Lib.SendSync
 open Pulse.Class.Duplicable
+open PulseCore.Observability
 
 val inv (i: iname) (p: slprop) : slprop
 
+ghost fn move i p l1 l2
+    (fwd: unit -> stt_ghost unit emp_inames (on l1 p) (fun _ -> on l2 p))
+    (bwd: unit -> stt_ghost unit emp_inames (on l2 p) (fun _ -> on l1 p))
+  requires on l1 (inv i p)
+  ensures on l2 (inv i p)
+
 instance val placeless_inv i p {| placeless p |} : placeless (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)
+
+ghost fn new_invariant (p: slprop)
+  requires p
+  returns i: iname
+  ensures inv i p
+
+inline_for_extraction noextract
+ghost fn with_inv_g u#a (a: Type u#a)
+    is (i: iname { not (mem_inv is i) }) (p: slprop) pre (post: a->slprop)
+    (k: unit -> stt_ghost a is (pre ** p) (fun x -> post x ** p))
+  opens add_inv is i
+  preserves inv i p
+  requires later_credit 1
+  requires pre
+  returns x:a
+  ensures post x
+
+inline_for_extraction noextract
+atomic fn with_inv_atomic 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 #Observable is (pre ** p) (fun x -> post x ** p))
+  opens add_inv is i
+  preserves inv i p
+  requires later_credit 1
+  requires pre
+  returns x:a
+  ensures post x
+
+inline_for_extraction noextract
+fn with_inv_stt 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 #Observable is (pre ** p) (fun x -> post x ** p))
+  preserves inv i p
+  requires pre
+  returns x:a
+  ensures post x