wi

Author: gebner

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

@@ -0,0 +1,78 @@
+module Pulse.Lib.BetterInv
+#lang-pulse
+open Pulse.Lib.Core
+open Pulse.Lib.SendSync
+open Pulse.Class.Duplicable
+module C = Pulse.Lib.Core
+
+unfold
+let move_tag0 l1 l2 p
+  (f: unit -> stt_ghost unit emp_inames (on l1 p) (fun _ -> on l2 p))
+  = emp
+
+let move_tag l1 l2 p f g =
+  move_tag0 l1 l2 p f ** move_tag0 l2 l1 p g
+
+let inv (i: iname) (p: slprop) =
+  exists* l l' f g.
+  loc l ** move_tag l l' p f g **
+  C.inv i (on l' p)
+
+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 inst l2 l') (aux inst l' l2);
+      loc_dup l2;
+      fold inv i p;
+      on_intro (inv i p);
+    }
+  }
+}
+
+ghost fn is_sync_inv i p {| is_sync p |} : is_sync (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. _;
+    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 _ {
+      ghost fn f' ()
+        requires on l2 p
+        ensures on l' p
+      {
+        is_sync_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;
+      };
+      fold move_tag l2 l' p f' g';
+      loc_dup l2;
+      fold inv i p;
+      on_intro (inv i p);
+    }
+  }
+}
+
+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)) ();
+  loc_dup _;
+  fold move_tag l l' p f g;
+  fold inv i p;
+  fold inv i p;
+}
+
+instance duplicable_inv i p : duplicable (inv i p) =
+  { dup_f = dup_inv i p }

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

@@ -0,0 +1,11 @@
+module Pulse.Lib.BetterInv
+#lang-pulse
+open Pulse.Lib.Core
+open Pulse.Lib.SendSync
+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 duplicable_inv i p : duplicable (inv i p)

test/Kuiper.fst

@@ -0,0 +1,17 @@
+module Kuiper
+open Pulse
+open Pulse.Lib.SendSync
+#lang-pulse
+
+assume val (forall+) #a (p: a->slprop) : slprop
+
+assume val gpu_global_mem : loc_id
+assume val gpu_shared_mem (blkid: nat) : loc_id
+assume val gpu_thread (blkid: nat) (thrid: nat) : loc_id
+
+let natlt n = i:nat { i < n }
+
+fn launch_kernel
+  (nblk nthr: nat)
+  (k: unit -> stt unit
+    (requires on gpu_global_mem (forall+ (blkid: natlt nblk) (thrid: natlt nthr)))