Merge pull request #140 from mtzguido/par

Restore parallel examples

Steel.fst.config.json

@@ -13,6 +13,7 @@
     "share/steel/examples/pulse/by-example",
     "share/steel/examples/pulse/lib",
     "share/steel/examples/pulse/parallel",
+    "share/steel/examples/pulse/parix",
     "share/steel/examples/pulse/dice",
     "share/steel/examples/pulse/dice/cbor",
     "share/steel/examples/pulse/dice/dpe",

share/steel/examples/pulse/Makefile

@@ -3,7 +3,7 @@ STEEL_SHARE = ../../
 # the root (../../../..) since the OPAM package will detach the share
 # directory from the rest of the repo.
 
-INCLUDE_DIRS=bug-reports by-example lib dice/cbor dice/common dice/dpe dice/engine dice/l0 parallel .
+INCLUDE_DIRS=bug-reports by-example lib dice/cbor dice/common dice/dpe dice/engine dice/l0 parallel parix .
 CACHE_DIR=.cache
 SRC_DIRS=$(addprefix $(STEEL_SHARE)/examples/pulse/, $(INCLUDE_DIRS))
 FSTAR_FILES=$(wildcard $(addsuffix /*.fst, $(SRC_DIRS))) $(wildcard $(addsuffix /*.fsti, $(SRC_DIRS)))

share/steel/examples/pulse/Pulse.fst.config.json

@@ -15,6 +15,7 @@
     "by-example",
     "lib",
     "parallel",
+    "parix",
     "dice",
     "dice/cbor",
     "dice/dpe",

share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fst

@@ -0,0 +1,34 @@
+module Pulse.Lib.Fixpoints
+
+open Pulse.Lib.Core
+
+let rec fix_1 (#a : Type) (#b : a -> Type)
+  (ff : (x:a -> (y:a{y << x} -> Tot (b y)) -> Tot (b x)))
+  : x:a -> Tot (b x)
+  = fun x -> ff x (fix_1 ff)
+
+let rec fix_ghost_1 (#a : Type0) (#b : a -> Type0)
+  (ff : (x:a -> (y:a{y << x} -> GTot (b y)) -> GTot (b x)))
+  : x:a -> GTot (b x)
+  = fun x -> ff x (fix_ghost_1 ff)
+
+let fix_stt_ghost_1 (#a : Type) (#b : a -> Type) (#pre : a -> vprop) (#post : (x:a -> b x -> vprop))
+  (ff : (x:a -> (y:a{y << x} -> stt_ghost (b y) emp_inames (pre y) (post y)) -> stt_ghost (b x) emp_inames (pre x) (post x)))
+  : x:a -> stt_ghost (b x) emp_inames (pre x) (post x)
+  = fix_1 #a #(fun x -> stt_ghost (b x) emp_inames (pre x) (post x)) ff
+
+friend Pulse.Lib.Core
+open Steel.ST
+open Steel.ST.Effect
+
+(* No termination check needed by dropping into STT *)
+
+let fix_stt_1 (#a : Type) (#b : a -> Type) (#pre : a -> vprop) (#post : (x:a -> b x -> vprop))
+  (kk : ((y:a -> stt (b y) (pre y) (post y)) -> x:a -> stt (b x) (pre x) (post x)))
+  : x:a -> stt (b x) (pre x) (post x)
+  =
+  let rec f (x:a) : STT (b x) (pre x) (post x) = 
+    kk (fun y () -> f y) x ()
+  in
+  let ff (x:a) : stt (b x) (pre x) (post x) = fun () -> f x in
+  ff

share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fsti

@@ -0,0 +1,19 @@
+module Pulse.Lib.Fixpoints
+
+open Pulse.Lib.Core
+
+val fix_1 (#a : Type) (#b : a -> Type)
+  (ff : (x:a -> (y:a{y << x} -> Tot (b y)) -> Tot (b x)))
+  : x:a -> Tot (b x)
+
+val fix_ghost_1 (#a : Type0) (#b : a -> Type0)
+  (ff : (x:a -> (y:a{y << x} -> GTot (b y)) -> GTot (b x)))
+  : x:a -> GTot (b x)
+
+val fix_stt_ghost_1 (#a : Type) (#b : a -> Type) (#pre : a -> vprop) (#post : (x:a -> b x -> vprop))
+  (ff : (x:a -> (y:a{y << x} -> stt_ghost (b y) emp_inames (pre y) (post y)) -> stt_ghost (b x) emp_inames (pre x) (post x)))
+  : x:a -> stt_ghost (b x) emp_inames (pre x) (post x)
+
+val fix_stt_1 (#a : Type) (#b : a -> Type) (#pre : a -> vprop) (#post : (x:a -> b x -> vprop))
+  (ff : (y:a -> stt (b y) (pre y) (post y)) -> (x:a -> stt (b x) (pre x) (post x)))
+  : x:a -> stt (b x) (pre x) (post x)

share/steel/examples/pulse/lib/Pulse.Lib.Par.Pledge.fsti

@@ -7,6 +7,10 @@ val pledge (opens:inames) (f:vprop) (v:vprop) : vprop
 let pledge_any (f:vprop) (v:vprop) : vprop =
   exists* is. pledge is f v
 
+unfold
+let pledge0 (f:vprop) (v:vprop) : vprop =
+  pledge emp_inames f v
+
 val pledge_sub_inv (os1:inames) (os2:inames{inames_subset os1 os2}) (f:vprop) (v:vprop)
   : stt_ghost unit emp_inames (pledge os1 f v) (fun _ -> pledge os2 f v)
 

share/steel/examples/pulse/parix/Async.Examples.fst

@@ -0,0 +1,32 @@
+module Async.Examples
+
+open Pulse.Lib.Pervasives
+open Async
+
+```pulse
+fn mock_http_req (cb : (string -> stt int emp (fun _ -> emp)))
+  requires emp
+  returns _:int
+  ensures emp
+{
+  let t1 = async (fun () -> cb "/index.html");
+  let t2 = async (fun () -> cb "/whatever");
+  let v1 = await t1;
+  let v2 = await t2;
+  let v = v1+v2;
+  v
+}
+```
+
+```pulse
+fn mock_http_req2_retasync (cb : (string -> stt int emp (fun _ -> emp)))
+  requires emp
+  returns r:(asynch int (fun _ -> emp))
+  ensures async_joinable r
+{
+  let t1 = async (fun () -> cb "/index.html");
+  let t2 = async (fun () -> cb "/whatever");
+  let v1 = await t1;
+  t2
+}
+```

share/steel/examples/pulse/parix/Async.fst

@@ -0,0 +1,128 @@
+module Async
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Par.Pledge
+open UnixFork
+
+(* Pulse will currently not recognize calls to anything other than
+top-level names, so this allows to force it. *)
+val now
+  (#a #pre #post : _)
+  (f : unit -> stt a pre post)
+  : unit -> stt a pre post
+let now f () = f ()
+
+let ref_solves_post (#a:Type0) (r:ref (option a)) (post : a -> vprop) : vprop =
+  exists* (v:a). pts_to r (Some v) ** post v
+
+(* NB: The vprop is not used here, so why the index? Only to make
+it easier for users to call await, as the post should be unified
+and hence the user would not need to explicitly repeat it. Unless
+we can fill it from the context...? *)
+let asynch (a:Type0) (post : a -> vprop) : Type0 =
+  ref (option a) & thread
+
+let async_joinable #a #post h =
+  joinable (snd h) ** pledge emp_inames (done (snd h)) (ref_solves_post (fst h) post)
+
+// val async
+//   (#a : Type0)
+//   (#pre : vprop)
+//   (#post : a -> vprop)
+//   (f : unit -> stt a pre post)
+//   : stt (asynch a post) pre (fun h -> async_joinable h)
+// let async #a #pre #post f =
+//   bind_stt (alloc None) (fun h ->
+//   let th = fork (fun () -> bind_stt (f ()) (fun (x:a) -> h := Some a)) in
+//   (| h, th |))
+
+```pulse
+fn async_fill
+  (#a : Type0)
+  (#pre : vprop)
+  (#post : (a -> vprop))
+  (f : (unit -> stt a pre (fun x -> post x)))
+  (r : ref (option a))
+  (_:unit)
+  requires pre ** pts_to r None
+  returns _ : unit
+  ensures ref_solves_post r post
+{
+  // Very nice!
+  let v : a = f ();
+  r := Some v;
+  fold ref_solves_post r post;
+  ()
+}
+```
+
+```pulse
+fn __async
+  (#a : Type0)
+  (#pre : vprop)
+  (#post : (a -> vprop))
+  (f : (unit -> stt a pre post))
+  requires pre
+  returns h : asynch a post
+  ensures async_joinable h
+{
+  let r = alloc (None #a);
+//   let th = fork #(pre ** pts_to r None) #(exists_ (fun (v:a) -> pts_to r (Some v) ** post v))
+//              (fun () -> async_fill #a #pre #post f r ());
+
+  // let k
+  //   : (unit -> stt u#0 unit (pre ** pts_to u#0 #(option u#0 a) r #full_perm (None u#0 #a))
+  //                           (fun () -> ref_solves_post #a r post))
+  //   = (fun () -> async_fill #a #pre #post f r ());
+  // let th = fork #(pre ** pts_to r None) #(ref_solves_post r post)
+  let th = fork #(pre ** pts_to r None) #(ref_solves_post r post)
+                (fun () -> magic()); // FIXME... it's the thing above (or below)
+                // (async_fill #a #pre #post f r);
+  let res = ( r, th );
+
+  assert (joinable th);
+  assert (pledge emp_inames (done th) (ref_solves_post r post));
+  rewrite (joinable th ** pledge emp_inames (done th) (ref_solves_post r post))
+       as (async_joinable #_ #post res);
+  res
+}
+```
+let async = __async
+
+```pulse
+fn __await
+  (#a : Type0)
+  (#post : (a -> vprop))
+  (h : asynch a post)
+  requires async_joinable h
+  returns x:a
+  ensures post x
+{
+  let r = fst h;
+  let th = snd h;
+  unfold async_joinable h;
+  assert (joinable th);
+  join th; (* join the thread *)
+  assert (done th);
+  rewrite (done th) as (done (snd h));
+  redeem_pledge emp_inames (done (snd h)) (ref_solves_post r post);
+  assert (ref_solves_post r post);
+  unfold ref_solves_post r post;
+  with vv. assert (pts_to r (Some vv));
+  drop_ (done th);
+
+  assert (post vv);
+  assert (pts_to r (Some vv));
+
+  let vo = !r;
+  free r;
+  match vo {
+    Some v -> {
+      rewrite (post vv) as (post v);
+      assert (post v);
+      v
+    }
+  }
+}
+```
+let await = __await

share/steel/examples/pulse/parix/Async.fsti

@@ -0,0 +1,24 @@
+module Async
+
+open Pulse.Lib.Pervasives
+
+val asynch (a:Type0) (post : a -> vprop) : Type0
+
+val async_joinable
+  (#a : Type0)
+  (#post : a -> vprop)
+  (h : asynch a post)
+  : vprop
+
+val async
+  (#a : Type0)
+  (#pre : vprop)
+  (#post : (a -> vprop))
+  (f : (unit -> stt a pre post))
+  : stt (asynch a post) pre (fun h -> async_joinable h)
+
+val await
+  (#a : Type0)
+  (#post : (a -> vprop))
+  (h : asynch a post)
+  : stt a (async_joinable h) (fun x -> post x)

share/steel/examples/pulse/parix/Makefile

@@ -0,0 +1,10 @@
+all: verify
+
+# assuming share/steel/examples/pulse/parix
+STEEL_HOME ?= ../../../../..
+
+FSTAR_OPTIONS = --include $(STEEL_HOME)/lib/steel/pulse
+
+COMPAT_INDEXED_EFFECTS=
+
+include $(STEEL_HOME)/share/steel/Makefile.include