From 3055cb40fe67d78ef7ade4c7a4477075a2a571a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 13 Dec 2023 16:12:44 -0800
Subject: [PATCH 1/3] LList.Invariant: remove workaround

Problem seems to be gone.. but still we don't exactly know why.
---
 share/steel/examples/steel/LList.Invariant.fst | 2 --
 1 file changed, 2 deletions(-)

diff --git a/share/steel/examples/steel/LList.Invariant.fst b/share/steel/examples/steel/LList.Invariant.fst
index 80da9d5f9..7e8b87a25 100644
--- a/share/steel/examples/steel/LList.Invariant.fst
+++ b/share/steel/examples/steel/LList.Invariant.fst
@@ -65,8 +65,6 @@ let llist = llist'
 (* Helper lemmas/rewritings *)
 
 let intro_llist_nil a =
-  ();
-  ();
   rewrite_slprop emp (llist null_llist [])
     (fun m -> pure_interp (null_llist #a == null_llist) m;
            norm_spec [delta; zeta] ((llist (null_llist #a) [])))

From 173e6674be7266b331ca5cd31b4a51e9c7a37782 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 31 Aug 2023 16:08:06 -0700
Subject: [PATCH 2/3] Pulse.Lib.Fixpoints: basic combinators for recursion

---
 .../pulse/lib/Pulse.Lib.Fixpoints.fst         | 34 +++++++++++++++++++
 .../pulse/lib/Pulse.Lib.Fixpoints.fsti        | 19 +++++++++++
 2 files changed, 53 insertions(+)
 create mode 100644 share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fst
 create mode 100644 share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fsti

diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fst b/share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fst
new file mode 100644
index 000000000..7c0e31257
--- /dev/null
+++ b/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
diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fsti b/share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fsti
new file mode 100644
index 000000000..dfc8be38c
--- /dev/null
+++ b/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)

From 0297954e963901be9d7c1cc619b41001e48d4313 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 19 Dec 2023 10:58:07 -0800
Subject: [PATCH 3/3] examples: Parallel examples restored

---
 Steel.fst.config.json                         |   1 +
 share/steel/examples/pulse/Makefile           |   2 +-
 .../examples/pulse/Pulse.fst.config.json      |   1 +
 .../pulse/lib/Pulse.Lib.Par.Pledge.fsti       |   4 +
 .../examples/pulse/parix/Async.Examples.fst   |  32 +
 share/steel/examples/pulse/parix/Async.fst    | 128 ++++
 share/steel/examples/pulse/parix/Async.fsti   |  24 +
 share/steel/examples/pulse/parix/Makefile     |  10 +
 .../examples/pulse/parix/ParallelFor.fst      | 641 ++++++++++++++++++
 .../pulse/parix/Promises.Examples.fst         | 111 +++
 .../pulse/parix/Promises.Examples3.fst        | 152 +++++
 .../examples/pulse/parix/Promises.Temp.fsti   |  39 ++
 .../pulse/parix/TaskPool.Examples.fst         | 124 ++++
 share/steel/examples/pulse/parix/TaskPool.fst |  72 ++
 .../steel/examples/pulse/parix/TaskPool.fsti  |  89 +++
 .../steel/examples/pulse/parix/UnixFork.fsti  |  21 +
 16 files changed, 1450 insertions(+), 1 deletion(-)
 create mode 100644 share/steel/examples/pulse/parix/Async.Examples.fst
 create mode 100644 share/steel/examples/pulse/parix/Async.fst
 create mode 100644 share/steel/examples/pulse/parix/Async.fsti
 create mode 100644 share/steel/examples/pulse/parix/Makefile
 create mode 100644 share/steel/examples/pulse/parix/ParallelFor.fst
 create mode 100644 share/steel/examples/pulse/parix/Promises.Examples.fst
 create mode 100644 share/steel/examples/pulse/parix/Promises.Examples3.fst
 create mode 100644 share/steel/examples/pulse/parix/Promises.Temp.fsti
 create mode 100644 share/steel/examples/pulse/parix/TaskPool.Examples.fst
 create mode 100644 share/steel/examples/pulse/parix/TaskPool.fst
 create mode 100644 share/steel/examples/pulse/parix/TaskPool.fsti
 create mode 100644 share/steel/examples/pulse/parix/UnixFork.fsti

diff --git a/Steel.fst.config.json b/Steel.fst.config.json
index 8ca4ea9ae..5556c43a9 100644
--- a/Steel.fst.config.json
+++ b/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",
diff --git a/share/steel/examples/pulse/Makefile b/share/steel/examples/pulse/Makefile
index 81bfa606b..1f85586a6 100755
--- a/share/steel/examples/pulse/Makefile
+++ b/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)))
diff --git a/share/steel/examples/pulse/Pulse.fst.config.json b/share/steel/examples/pulse/Pulse.fst.config.json
index f9454fee6..16bf8e925 100644
--- a/share/steel/examples/pulse/Pulse.fst.config.json
+++ b/share/steel/examples/pulse/Pulse.fst.config.json
@@ -15,6 +15,7 @@
     "by-example",
     "lib",
     "parallel",
+    "parix",
     "dice",
     "dice/cbor",
     "dice/dpe",
diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Par.Pledge.fsti b/share/steel/examples/pulse/lib/Pulse.Lib.Par.Pledge.fsti
index 7f6c543f5..b34287927 100644
--- a/share/steel/examples/pulse/lib/Pulse.Lib.Par.Pledge.fsti
+++ b/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)
 
diff --git a/share/steel/examples/pulse/parix/Async.Examples.fst b/share/steel/examples/pulse/parix/Async.Examples.fst
new file mode 100644
index 000000000..05daafec6
--- /dev/null
+++ b/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
+}
+```
diff --git a/share/steel/examples/pulse/parix/Async.fst b/share/steel/examples/pulse/parix/Async.fst
new file mode 100644
index 000000000..01d3a0f86
--- /dev/null
+++ b/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
diff --git a/share/steel/examples/pulse/parix/Async.fsti b/share/steel/examples/pulse/parix/Async.fsti
new file mode 100644
index 000000000..9c571ec88
--- /dev/null
+++ b/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)
diff --git a/share/steel/examples/pulse/parix/Makefile b/share/steel/examples/pulse/parix/Makefile
new file mode 100644
index 000000000..4e6114848
--- /dev/null
+++ b/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
diff --git a/share/steel/examples/pulse/parix/ParallelFor.fst b/share/steel/examples/pulse/parix/ParallelFor.fst
new file mode 100644
index 000000000..cf0d7ef1d
--- /dev/null
+++ b/share/steel/examples/pulse/parix/ParallelFor.fst
@@ -0,0 +1,641 @@
+module ParallelFor
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Fixpoints
+open TaskPool
+open FStar.Real
+open Pulse.Lib.Par.Pledge
+
+```pulse
+ghost
+fn aux_squash_pledge (f v : vprop) (_:unit)
+  requires f ** pledge emp_inames f (pledge emp_inames f v)
+  ensures f ** v
+{
+  redeem_pledge emp_inames f (pledge emp_inames f v);
+  redeem_pledge emp_inames f v
+}
+```
+
+```pulse
+ghost
+fn squash_pledge (f v : vprop)
+  requires pledge emp_inames f (pledge emp_inames f v)
+  ensures pledge emp_inames f v
+{
+  make_pledge emp_inames f v
+   (pledge emp_inames f (pledge emp_inames f v))
+   (aux_squash_pledge f v)
+}
+```
+
+let div_perm (p:perm) (n:pos) : perm =
+  let open Steel.FractionalPermission in
+  MkPerm ((MkPerm?.v p) /. of_int n)
+
+(* Basic sketch of a parallel for *)
+
+(* First, a sequential one. *)
+
+val range : (nat -> vprop) -> i:nat -> j:nat -> vprop
+let rec range p i j : Tot vprop (decreases j-i) =
+  if i < j
+  then p i ** range p (i+1) j
+  else emp
+
+(* The precondition on i/j/k is needed otherwise the LHS can be stronger. *)
+val p_join_equiv (p : nat -> vprop) (i j k : nat) (_ : squash (i <= j /\ j <= k))
+  : Tot (vprop_equiv (range p i j ** range p j k) (range p i k)) (decreases j-i)
+let rec p_join_equiv p i j k _ =
+  if i = j
+  then (
+    assert (range p i j == emp);
+    vprop_equiv_unit _
+  )
+  else (
+    let eq : vprop_equiv (range p i j ** range p j k) ((p i ** range p (i+1) j) ** range p j k) =
+      vprop_equiv_refl _
+    in
+    let eq : vprop_equiv (range p i j ** range p j k) (p i ** (range p (i+1) j ** range p j k)) =
+      vprop_equiv_trans _ _ _ eq
+        (vprop_equiv_assoc _ _ _)
+    in
+    let eq : vprop_equiv (range p i j ** range p j k) (p i ** range p (i+1) k) =
+      vprop_equiv_trans _ _ _ eq
+        (vprop_equiv_cong _ _ _ _ (vprop_equiv_refl _) (p_join_equiv p (i+1) j k ()))
+    in
+    eq
+  )
+
+val p_join_last_equiv (p : nat -> vprop) (n : pos)
+  : Tot (vprop_equiv (range p 0 n) (range p 0 (n-1) ** p (n-1)))
+
+let rec p_join_last_equiv p n =
+  if n = 1 then vprop_equiv_comm _ _
+  else (
+    let eq : vprop_equiv (range p 0 n) (range p 0 (n-1) ** range p (n-1) n) =
+      vprop_equiv_sym _ _ (p_join_equiv p 0 (n-1) n ())
+    in
+    let eq : vprop_equiv (range p 0 n) (range p 0 (n-1) ** (p (n-1) ** emp)) =
+      vprop_equiv_trans _ _ _ eq
+        (vprop_equiv_refl _)
+    in
+    let eq : vprop_equiv (range p 0 n) (range p 0 (n-1) ** (emp ** p (n-1))) =
+      vprop_equiv_trans _ _ _ eq
+        (vprop_equiv_cong _ _ _ _ (vprop_equiv_refl _) (vprop_equiv_comm _ _)) // (vprop_equiv_unit _)))
+    in
+    let eq : vprop_equiv (range p 0 n) (range p 0 (n-1) ** p (n-1)) =
+      vprop_equiv_trans _ _ _ eq
+        (vprop_equiv_cong _ _ _ _ (vprop_equiv_refl _) (vprop_equiv_unit _))
+    in
+    eq
+  )
+
+val p_combine_equiv (p1 p2 : nat -> vprop) (i j : nat)
+  : Tot (vprop_equiv (range p1 i j ** range p2 i j) (range (fun i -> p1 i ** p2 i) i j))
+let p_combine_equiv p1 p2 i j = magic()
+
+let rewrite_ = Pulse.Lib.Core.rewrite
+
+```pulse
+ghost
+fn p_join (p : (nat->vprop)) (i j k : nat) (_ : squash (i <= j /\ j <= k))
+  requires range p i j ** range p j k
+  ensures range p i k
+{
+  rewrite_ _ _ (p_join_equiv p i j k ())
+}
+```
+
+```pulse
+ghost
+fn p_split (p : (nat->vprop)) (i j k : nat) (_ : squash (i <= j /\ j <= k))
+  requires range p i k
+  ensures range p i j ** range p j k
+{
+  rewrite_ _ _ (vprop_equiv_sym _ _ (p_join_equiv p i j k ()))
+}
+```
+
+```pulse
+ghost
+fn p_join_last (p : (nat->vprop)) (n : nat) (_ : squash (n > 0))
+  requires range p 0 (n-1) ** p (n-1)
+  ensures range p 0 n
+{
+  rewrite_ _ _ (vprop_equiv_sym _ _ (p_join_last_equiv p n))
+}
+```
+
+```pulse
+ghost
+fn p_split_last (p : (nat->vprop)) (n : nat) (_ : squash (n > 0))
+  requires range p 0 n
+  ensures range p 0 (n-1) ** p (n-1)
+{
+  rewrite_ _ _ (p_join_last_equiv p n)
+}
+```
+
+```pulse
+ghost
+fn p_combine (p1 p2 : (nat->vprop)) (i j : nat)
+  requires range p1 i j ** range p2 i j
+  ensures range (fun i -> p1 i ** p2 i) i j
+{
+  rewrite_ _ _ (p_combine_equiv p1 p2 i j)
+//   rewrite_ _ _ (vprop_equiv_sym _ _ (p_combine_equiv p1 p2 i j))
+}
+```
+
+```pulse
+ghost
+fn p_uncombine (p1 p2 : (nat->vprop)) (i j : nat)
+  requires range (fun i -> p1 i ** p2 i) i j
+  ensures range p1 i j ** range p2 i j
+{
+//   rewrite_ _ _ (p_combine_equiv p1 p2 i j)
+  rewrite_ _ _ (vprop_equiv_sym _ _ (p_combine_equiv p1 p2 i j))
+}
+```
+
+```pulse
+fn __simple_for
+   (pre post : (nat -> vprop))
+   (r : vprop) // This resource is passed around through iterations.
+   (f : (i:nat -> stt unit (r ** pre i) (fun () -> (r ** post i))))
+   (kk : (
+     (n : nat) ->
+     stt unit (r ** range pre 0 n) (fun _ -> r ** range post 0 n)
+   ))
+   (n : nat)
+   requires r ** range pre 0 n
+   ensures r ** range post 0 n
+{
+  (* Couldn't use a while loop here, weird errors, try again. *)
+  if (n = 0) {
+    rewrite (range pre 0 n) as emp;
+    rewrite emp as (range post 0 n);
+    ()
+  } else {
+    // rewrite (range pre 0 n) as (range pre (reveal (hide 0)) (reveal (hide n)));
+    p_split_last pre n ();
+    f (n-1);
+    kk (n-1);
+    p_join_last post n ();
+    ()
+  }
+}
+```
+
+let simple_for  :
+     (pre : (nat -> vprop)) ->
+     (post : (nat -> vprop)) ->
+     (r : vprop) -> // This resource is passed around through iterations.
+     (f : (i:nat -> stt unit (r ** pre i) (fun () -> r ** post i))) ->
+     (n : nat) ->
+     stt unit (r ** range pre 0 n) (fun _ -> r ** range post 0 n)
+  = 
+  fun pre post r f -> fix_stt_1 (__simple_for pre post r f)
+
+```pulse
+fn for_loop
+   (pre post : (nat -> vprop))
+   (r : vprop) // This resource is passed around through iterations.
+   (f : (i:nat -> stt unit (r ** pre i) (fun () -> (r ** post i))))
+   (lo hi : nat)
+   requires r ** range pre lo hi
+   ensures r ** range post lo hi
+{
+  (* TODO: implement by just shifting simple_for? *)
+  admit()
+}
+```
+
+
+assume val frac_n (n:pos) (p:pool) (e:perm)
+  : stt unit (pool_alive #e p)
+             (fun () -> range (fun i -> pool_alive #(div_perm e n) p) 0 n)
+
+assume val unfrac_n (n:pos) (p:pool) (e:perm)
+  : stt unit (range (fun i -> pool_alive #(div_perm e n) p) 0 n)
+             (fun () -> pool_alive #e p)
+
+#set-options "--print_implicits --print_universes"
+
+// FIXME: arguments with defaults (i.e. metaargs with tactics)
+// make functions not be recognized by Pulse
+val gspawn_
+  (#pre #post : _)
+  (#e : perm)
+  (p:pool) (f : unit -> stt unit pre (fun _ -> post))
+  : stt unit (pool_alive #e p ** pre)
+             (fun prom -> pool_alive #e p ** pledge emp_inames (pool_done p) post)
+let gspawn_ p f = TaskPool.spawn_ p f
+
+```pulse
+fn spawned_f_i 
+  (p:pool)
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (e:perm)
+  (f : (i:nat -> stt unit (pre i) (fun () -> post i)))
+  (i:nat)
+  requires emp ** (pre i ** pool_alive #e p)
+  ensures emp ** (pledge emp_inames (pool_done p) (post i) ** pool_alive #e p)
+{
+  gspawn_ #(pre i) #(post i) #e p (fun () -> f i)
+}
+```
+
+// In pulse, using fixpoint combinator below. Should be a ghost step eventually
+```pulse
+fn __redeem_range
+  (p : (nat -> vprop))
+  (f : vprop)
+  (kk : (
+    (n:nat) ->
+    stt unit (f ** range (fun i -> pledge emp_inames f (p i)) 0 n)
+             (fun _ -> f ** range p 0 n)
+  ))
+  (n : nat)
+  requires f ** range (fun i -> pledge emp_inames f (p i)) 0 n
+  ensures f ** range p 0 n
+{
+  if (n = 0) {
+    rewrite (range (fun i -> pledge emp_inames f (p i)) 0 n) as emp;
+    rewrite emp as range p 0 n;
+    ()
+  } else {
+    p_split_last (fun i -> pledge emp_inames f (p i)) n ();
+    redeem_pledge _ f (p (n-1));
+    kk (n-1);
+    p_join_last p n ();
+    ()
+  }
+}
+```
+
+let redeem_range :
+  (p : (nat -> vprop)) ->
+  (f : vprop) ->
+    (n:nat) ->
+    stt unit (f ** range (fun i -> pledge emp_inames f (p i)) 0 n)
+             (fun _ -> f ** range p 0 n)
+  =
+  fun p f -> fix_stt_1 (__redeem_range p f)
+
+```pulse
+fn
+parallel_for
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (f : (i:nat -> stt unit (pre i) (fun () -> (post i))))
+  (n : pos)
+  requires range pre 0 n
+  ensures range post 0 n
+{
+  let p = setup_pool 42;
+  (* Use a normal for loop to *spawn* each task *)
+  
+  (* First, share the pool_alive permission among all n tasks. *)
+  assert (pool_alive #full_perm p);
+  frac_n n p full_perm;
+  
+  p_combine pre (fun i -> pool_alive #(div_perm full_perm n) p) 0 n;
+
+  simple_for
+    (fun i -> pre i ** pool_alive #(div_perm full_perm n) p)
+    (fun i -> pledge emp_inames (pool_done p) (post i) ** pool_alive #(div_perm full_perm n) p)
+    emp // Alternative: pass pool_alive p here and forget about the n-way split. See below.
+    (spawned_f_i p pre post (div_perm full_perm n) f)
+    n;
+    
+  p_uncombine (fun i -> pledge emp_inames (pool_done p) (post i)) (fun i -> pool_alive #(div_perm full_perm n) p) 0 n;
+  unfrac_n n p full_perm;
+  teardown_pool p;
+  
+  redeem_range post (pool_done p) n;
+
+  drop_ (pool_done p);
+
+  ()
+}
+```
+
+
+```pulse
+fn spawned_f_i_alt
+  (p:pool)
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (f : (i:nat -> stt unit (pre i) (fun () -> post i)))
+  (i:nat)
+  requires pool_alive p ** pre i
+  ensures pool_alive p ** pledge emp_inames (pool_done p) (post i)
+{
+  gspawn_ #(pre i) #(post i) #full_perm p (fun () -> f i)
+}
+```
+
+(* Alternative; not splitting the pool_alive resource. We are anyway
+spawning sequentially. *)
+```pulse
+fn
+parallel_for_alt
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (f : (i:nat -> stt unit (pre i) (fun () -> (post i))))
+  (n : pos)
+  requires range pre 0 n
+  ensures range post 0 n
+{
+  let p = setup_pool 42;
+
+  simple_for
+    pre
+    (fun i -> pledge emp_inames (pool_done p) (post i))
+    (pool_alive p)
+    (spawned_f_i_alt p pre post f)
+    n;
+    
+  teardown_pool p;
+  redeem_range post (pool_done p) n;
+  drop_ (pool_done p);
+  ()
+}
+```
+
+#push-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection'"
+#push-options "--retry 2 --ext 'pulse:rvalues'" // GM: Part of this VC fails on batch mode, not on ide...
+
+let wsr_loop_inv_f
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (full_post : (nat -> vprop))
+  (n : pos)
+  (i : ref int)
+  (b:bool)
+  : Tot vprop
+  =
+  exists* (ii:nat).
+       pts_to i ii
+    ** full_post ii
+    ** range post ii n
+    ** pure (b == (Prims.op_LessThan ii n))
+
+let wsr_loop_inv_tf
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (full_post : (nat -> vprop))
+  (n : pos)
+  (i : ref int)
+  : Tot vprop =
+  exists* (b:bool). wsr_loop_inv_f pre post full_post n i b
+  
+(* This can be ghost. *)
+```pulse
+fn
+__ffold
+  (p : (nat -> vprop))
+  (fp : (nat -> vprop))
+  (ss : (i:nat -> stt_ghost unit emp_inames (p i ** fp i) (fun () -> fp (i+1))))
+  (n : nat)
+  (kk: (
+        (i:nat) -> stt unit (pure (i <= n) ** fp i ** range p i n) (fun _ -> fp n)
+  ))
+  (i : nat)
+  requires pure (i <= n) ** fp i ** range p i n
+  ensures fp n
+{
+   if (i = n) {
+     rewrite (range p i n) as emp;
+     rewrite fp i as fp n;
+     ()
+   } else {
+     assert (fp i ** range p i n);
+     rewrite (range p i n) as (p i ** range p (i+1) n);
+     ss i;
+     kk (i+1);
+     ()
+   }
+}
+```
+let ffold
+  (p : (nat -> vprop))
+  (fp : (nat -> vprop))
+  (ss : (i:nat -> stt_ghost unit emp_inames (p i ** fp i) (fun () -> fp (i+1))))
+  (n:nat)
+  : (i:nat) -> stt unit (pure (i <= n) ** fp i ** range p i n) (fun _ -> fp n)
+  = fix_stt_1 (__ffold p fp ss n)
+
+(* This can be ghost. *)
+```pulse
+fn
+__funfold
+  (p : (nat -> vprop))
+  (fp : (nat -> vprop))
+  (ss : (i:nat -> stt_ghost unit emp_inames (fp (i+1)) (fun () -> p i ** fp i)))
+  (kk: (
+        (n:nat) -> stt unit (fp n) (fun _ -> fp 0 ** range p 0 n)
+  ))
+  (n : nat)
+  requires fp n
+  ensures fp 0 ** range p 0 n
+{
+   if (n = 0) {
+     rewrite fp n as fp 0;
+     rewrite emp as range p 0 n;
+     ()
+   } else {
+     assert (fp n);
+     rewrite fp n as fp ((n-1)+1);
+     ss (n-1);
+     assert (p (n-1) ** fp (n-1));
+     kk (n-1);
+     p_join_last p n ()
+   }
+}
+```
+let funfold
+  (p : (nat -> vprop))
+  (fp : (nat -> vprop))
+  (ss : (i:nat -> stt_ghost unit emp_inames (fp (i+1)) (fun () -> p i ** fp i)))
+  : (n:nat) -> stt unit (fp n) (fun _ -> fp 0 ** range p 0 n)
+  = fix_stt_1 (__funfold p fp ss)
+
+```pulse
+fn
+parallel_for_wsr
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (full_pre : (nat -> vprop))
+  (full_post : (nat -> vprop))
+  (f : (i:nat -> stt unit (pre i) (fun () -> post i)))
+  (unfold_pre : (i:nat -> stt_ghost unit emp_inames (full_pre (i+1)) (fun () -> pre i ** full_pre i)))
+  (fold_post : (i:nat -> stt_ghost unit emp_inames (post i ** full_post i) (fun () -> full_post (i+1))))
+  (n : pos)
+  requires full_pre n ** full_post 0
+  ensures full_pre 0 ** full_post n
+{
+  funfold pre full_pre unfold_pre n;
+  parallel_for pre post f n;
+  ffold post full_post fold_post n 0
+}
+```
+
+assume
+val frame_stt_left
+  (#a:Type u#a)
+  (#pre:vprop) (#post:a -> vprop)
+  (frame:vprop)
+  (e:stt a pre post)
+  : stt a (frame ** pre) (fun x -> frame ** post x)
+
+#set-options "--ext pulse:guard_policy=SMTSync"
+
+```pulse
+fn h_for_task__
+  (p:pool)
+  (e:perm)
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (f : (i:nat -> stt unit (pre i) (fun () -> post i)))
+  (lo hi : nat)
+  (_:unit)
+  requires pool_alive #e p ** range pre lo hi
+  ensures pledge emp_inames (pool_done p) (range post lo hi)
+{
+  admit()
+}
+```
+
+```pulse
+fn h_for_task
+  (p:pool)
+  (e:perm)
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (f : (i:nat -> stt unit (pre i) (fun () -> post i)))
+  (lo hi : nat)
+  (_:unit)
+  requires pool_alive #e p ** range pre lo hi
+  ensures pledge emp_inames (pool_done p) (range post lo hi)
+{
+  if (hi - lo < 100) {
+    (* Too small, just run sequentially *)
+    drop_ (pool_alive #e p); // won't use the pool
+    for_loop pre post emp
+             (fun i -> frame_stt_left emp (f i)) lo hi;
+
+    return_pledge emp_inames (pool_done p) (range post lo hi)
+  } else {
+    let mid = (hi+lo)/2;
+    assert (pure (lo <= mid /\ mid <= hi));
+
+    split_alive p e;
+    split_alive p (half_perm e);
+
+    p_split pre lo mid hi ();
+
+    gspawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre lo mid)
+            #(pledge emp_inames (pool_done p) (range post lo mid))
+            #(half_perm e)
+            p
+            (h_for_task__ p (half_perm (half_perm e)) pre post f lo mid);
+
+    gspawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre mid hi)
+            #(pledge emp_inames (pool_done p) (range post mid hi))
+            #(half_perm e)
+            p
+            (h_for_task__ p (half_perm (half_perm e)) pre post f mid hi);
+
+    (* We get this complicated pledge emp_inames from the spawns above. We can
+    massage it before even waiting. *)
+    assert (pledge emp_inames (pool_done p) (pledge emp_inames (pool_done p) (range post lo mid)));
+    assert (pledge emp_inames (pool_done p) (pledge emp_inames (pool_done p) (range post mid hi)));
+
+    squash_pledge (pool_done p) (range post lo mid);
+    squash_pledge (pool_done p) (range post mid hi);
+
+    join_pledge #emp_inames #(pool_done p) (range post lo mid) (range post mid hi);
+    rewrite_pledge #emp_inames #(pool_done p) (range post lo mid ** range post mid hi) (range post lo hi)
+        (fun () -> p_join post lo mid hi ());
+
+    (* Better *)
+    assert (pledge emp_inames (pool_done p) (range post lo hi));
+
+    drop_ (pool_alive #(half_perm e) p);
+
+    ()
+  }
+}
+```
+
+(* Assuming a wait that only needs epsilon permission. We would actually
+need one that takes epsilon permission + a pledge emp_inames for (1-e), or something
+similar. Otherwise we cannot rule out some other thread holding permission
+to the task pool, and we would not be allowed to free it. *)
+assume
+val wait_pool
+  (p:pool)
+  (e:perm)
+  : stt unit (pool_alive #e p) (fun _ -> pool_done p)
+
+```pulse
+fn
+parallel_for_hier
+  (pre : (nat -> vprop))
+  (post : (nat -> vprop))
+  (f : (i:nat -> stt unit (pre i) (fun () -> (post i))))
+  (n : pos)
+  requires range pre 0 n
+  ensures range post 0 n
+{
+  let p = setup_pool 42;
+
+  if (false) { // Checking that both branches would work
+    (* Spawning the first task: useless! Just call it! *)
+    assert (pool_alive #full_perm p);
+    split_alive p full_perm;
+
+    rewrite (pool_alive #(half_perm full_perm) p ** pool_alive #(half_perm full_perm) p)
+        as (pool_alive #one_half p ** pool_alive #one_half p);
+    assert (pool_alive #one_half p ** pool_alive #one_half p);
+
+
+    gspawn_ #(pool_alive #one_half p ** range pre 0 n)
+            #(pledge emp_inames (pool_done p) (range post 0 n))
+            #one_half
+            p
+            (h_for_task p one_half pre post f 0 n);
+
+    (* We get this complicated pledge emp_inames from the spawn above. We can
+    massage it before even waiting. *)
+    assert (pledge emp_inames (pool_done p) (pledge emp_inames (pool_done p) (range post 0 n)));
+
+    squash_pledge (pool_done p) (range post 0 n);
+
+    assert (pledge emp_inames (pool_done p) (range post 0 n));
+
+    wait_pool p one_half;
+
+    redeem_pledge emp_inames (pool_done p) (range post 0 n);
+
+    drop_ (pool_done p);
+  } else {
+    (* Directly calling is much easier, and actually better all around. *)
+    split_alive p full_perm;
+    h_for_task p (half_perm full_perm) pre post f 0 n ();
+
+    wait_pool p (half_perm full_perm);
+
+    assert (pool_done p);
+
+    redeem_pledge emp_inames (pool_done p) (range post 0 n);
+
+    drop_ (pool_done p);
+  }
+}
+```
+
diff --git a/share/steel/examples/pulse/parix/Promises.Examples.fst b/share/steel/examples/pulse/parix/Promises.Examples.fst
new file mode 100644
index 000000000..3d3f7ca11
--- /dev/null
+++ b/share/steel/examples/pulse/parix/Promises.Examples.fst
@@ -0,0 +1,111 @@
+module Promises.Examples
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Par.Pledge
+
+(* Assuming invariants *)
+
+[@@erasable]
+assume val inv : vprop -> Type0
+
+// should be ghost
+assume val mk_inv : p:vprop -> stt (inv p) p (fun _ -> emp)
+
+assume val with_inv
+  (#a:Type0) (#pre : vprop) (#post : (a -> vprop))
+  (#p:vprop)
+  (i:inv p)
+  ($f : unit -> stt_ghost a emp_inames (p ** pre) (fun r -> p ** post r))
+  : stt_ghost a emp_inames pre post
+
+assume val admit_ghost
+  (#a:Type0) (#pre : vprop) (#post : (a -> vprop))
+  (_:unit)
+  : stt_ghost a emp_inames pre post
+
+type abc = | A | B | C
+
+let invp (b:ref abc) (y:ref int) =
+  exists* (bb:abc). pts_to b #(half_perm full_perm) bb ** (if bb =B then pts_to y 42 else emp)
+
+(*
+```pulse
+fn test_aux (b : ref bool) (y : ref int)
+  requires pts_to b #(half_perm full_perm) true ** invp b y
+  ensures pts_to b #(half_perm full_perm) true ** pts_to y 42 ** invp b y
+{
+  unfold invp b y;
+  with bb.
+    assert (pts_to b #(half_perm full_perm) bb ** (if bb then pts_to y 42 else emp));
+  assert (pts_to b #(half_perm full_perm) true);
+  assert (pts_to b #(half_perm full_perm) bb);
+
+  // Automate?
+  pts_to_injective_eq #bool
+        #(half_perm full_perm) #(half_perm full_perm)
+        #true #bb
+        b;
+
+  // Automate?
+  rewrite (pts_to b #(half_perm full_perm) bb)
+       as (pts_to b #(half_perm full_perm) true);
+
+  gather b;
+
+  // Should automate
+  rewrite (pts_to b #(sum_perm (half_perm full_perm) (half_perm full_perm)) true)
+       as (pts_to b true);
+
+  assert (pts_to b #full_perm true);
+
+  b := false;
+
+  share b;
+
+  rewrite emp
+       as (if false then pts_to y 42 else emp);
+
+  intro_exists (fun (bb:bool) -> pts_to b #(half_perm full_perm) bb ** (if bb then pts_to y 42 else emp))
+    false;
+
+  fold invp b y;
+
+  ()
+}
+```
+(* Promising and redeeming in a single func *)
+```pulse
+fn test (b : ref bool) (y : ref int)
+  requires pts_to b false ** pts_to y yy
+  returns x:int
+  ensures promise (pts_to b true) (pts_to y 42)
+{
+  assert (pts_to b false);
+  share b;
+  assert (pts_to b #(half_perm full_perm) false);
+  assert (pts_to b #(half_perm full_perm) false ** emp);
+  rewrite emp
+       as `@(if false then pts_to y 42 else emp);
+  assert (pts_to b #(half_perm full_perm) false ** `@(if false then pts_to y 42 else emp));
+  assert (exists_ (fun (bb:bool) ->
+             pts_to b #(half_perm full_perm) bb ** (if bb then pts_to y 42 else emp)));
+  let i = mk_inv (exists_ (fun (bb:bool) ->
+             pts_to b #(half_perm full_perm) bb ** (if bb then pts_to y 42 else emp)));
+  y := 42;
+  make_promise
+    (pts_to b #(half_perm full_perm) true)
+    (pts_to y 42)
+    emp
+    (fun () -> with_inv
+                 #unit
+                 #(pts_to b true ** emp)
+                 #(fun () -> pts_to b false ** pts_to y 42)
+                 #(exists_ (fun (bb:bool) -> pts_to b #(half_perm full_perm) bb ** (if bb then pts_to y 42 else emp)))
+               i
+               (fun () -> test_aux b y)
+  );
+  admit()
+//   admit()
+}
+```
+*)
diff --git a/share/steel/examples/pulse/parix/Promises.Examples3.fst b/share/steel/examples/pulse/parix/Promises.Examples3.fst
new file mode 100644
index 000000000..eef2e3803
--- /dev/null
+++ b/share/steel/examples/pulse/parix/Promises.Examples3.fst
@@ -0,0 +1,152 @@
+module Promises.Examples3
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Par.Pledge
+module GR = Pulse.Lib.GhostReference
+
+assume val done : ref bool
+assume val res : ref (option int)
+assume val claimed : GR.ref bool
+
+let inv_p : vprop =
+  exists* (v_done:bool) (v_res:option int) (v_claimed:bool).
+       pts_to done #one_half v_done
+    ** pts_to res #one_half v_res
+    ** GR.pts_to claimed #one_half v_claimed
+    ** (if not v_claimed then pts_to res #one_half v_res else emp)
+    ** pure (v_claimed ==> v_done)
+    ** pure (v_done ==> Some? v_res)
+
+let goal : vprop =
+  exists* v_res. pts_to res #one_half v_res ** pure (Some? v_res)
+
+
+```pulse
+ghost
+fn proof
+   (i : inv inv_p) (_:unit)
+   requires pts_to done #one_half true ** GR.pts_to claimed #one_half false
+   ensures pts_to done #one_half true ** goal
+   opens add_inv emp_inames i
+{
+  with_invariants i {
+    unfold inv_p;
+    with v_done v_res v_claimed.
+      assert (pts_to done #one_half v_done
+              ** pts_to res #one_half v_res
+              ** GR.pts_to claimed #one_half v_claimed
+              ** (if not v_claimed then pts_to res #one_half v_res else emp)
+              ** pure (v_claimed ==> v_done)
+              ** pure (v_done ==> Some? v_res));
+
+    pts_to_injective_eq #_ #one_half #one_half #v_done #true done;
+    assert (pure (v_done == true));
+    
+    GR.gather2 #bool
+      claimed
+      #false #v_claimed;
+    assert (pure (v_claimed == false));
+
+    // NB: this step is very sensitive to ordering
+    rewrite ((if not v_claimed then pts_to res #one_half v_res else emp) ** emp)
+         as (pts_to res #one_half v_res ** (if not true then pts_to res #one_half v_res else emp));
+
+    GR.op_Colon_Equals claimed true;
+    
+    fold goal;
+    
+    GR.share2 #_ claimed;
+    
+    fold inv_p;
+    
+    drop_ (GR.pts_to claimed #one_half true);
+
+    ()
+  }
+}
+```
+
+```pulse
+fn setup (_:unit)
+   requires pts_to done v_done ** pts_to res v_res ** GR.pts_to claimed v_claimed
+   returns i:inv inv_p
+   ensures pts_to done #one_half false ** pledge (add_inv emp_inames i) (pts_to done #one_half true) goal
+{
+  done := false;
+  res := None;
+  GR.op_Colon_Equals claimed false;
+  
+  share2 #_ done;
+  share2 #_ res;
+  GR.share2 #_ claimed;
+  
+  rewrite (pts_to res #one_half None)
+       as (if not false then  pts_to res #one_half None else emp);
+       
+  fold inv_p;
+  
+  let i = new_invariant' inv_p;
+  
+  make_pledge
+    (add_inv emp_inames i)
+    (pts_to done #one_half true)
+    goal
+    (GR.pts_to claimed #one_half false)
+    (proof i);
+
+  i
+}
+```
+
+[@@expect_failure] // block is not atomic/ghost
+```pulse
+fn worker (i : inv inv_p) (_:unit)
+   requires pts_to done #one_half false
+   ensures pts_to done #one_half true
+{
+  with_invariants i {
+    unfold inv_p;
+    with v_done v_res v_claimed.
+      assert (pts_to done #one_half v_done
+              ** pts_to res #one_half v_res
+              ** GR.pts_to claimed #one_half v_claimed
+              ** (if not v_claimed then pts_to res #one_half v_res else emp)
+              ** pure (v_claimed ==> v_done)
+              ** pure (v_done ==> Some? v_res));
+
+    gather2 #_ done #false #v_done;
+    assert (pts_to done false);
+    
+    assert (pure (not v_claimed)); // contrapositive from v_done=false
+
+    rewrite (if not v_claimed then pts_to res #one_half v_res else emp)
+         as pts_to res #one_half v_res;
+         
+    gather2 #_ res #v_res #v_res;
+    assert (pts_to res v_res);
+    
+    
+    (* The main sketchy part here: two steps! But we see how
+    to fix this by either:
+      - Adding a lock and a ghost bool reference
+      - Using a monotonic reference for the result, so once we
+        set it to Some we know it must remain so. This allows
+        to not have a lock for this. It would be two with_invariant
+        steps.
+    *)
+    res := Some 42;
+    done := true;
+    
+    share2 #_ res;
+
+    rewrite (pts_to res #one_half (Some 42))
+        as (if not v_claimed then pts_to res #one_half (Some 42) else emp);
+        
+    share2 #_ done;
+    
+    fold inv_p;
+
+    ()
+  };
+}
+```
diff --git a/share/steel/examples/pulse/parix/Promises.Temp.fsti b/share/steel/examples/pulse/parix/Promises.Temp.fsti
new file mode 100644
index 000000000..f27bb9898
--- /dev/null
+++ b/share/steel/examples/pulse/parix/Promises.Temp.fsti
@@ -0,0 +1,39 @@
+module Promises.Temp
+
+(* A temporary interface that does not require anything
+to be ghost, and just works in stt. Clearly bogus, only to be used
+as a stepping stone. *)
+
+open Pulse.Lib.Pervasives
+
+val promise (f:vprop) (v:vprop) : vprop
+
+(* Anything that holds now holds in the future too. *)
+val return_promise (f:vprop) (v:vprop)
+  : stt unit v (fun _ -> promise f v)
+
+val make_promise (f:vprop) (v:vprop) (extra:vprop)
+  ($k : unit -> stt unit (f ** extra) (fun _ -> f ** v))
+  : stt unit extra (fun _ -> promise f v)
+
+val redeem_promise (f:vprop) (v:vprop)
+  : stt unit (f ** promise f v) (fun () -> f ** v)
+
+val bind_promise (#f:vprop) (#v1:vprop) (#v2:vprop)
+        (extra : vprop) // any better way to propagate context?
+        (k : unit -> stt unit (extra ** v1) (fun () -> promise f v2))
+  : stt unit (promise f v1 ** extra) (fun () -> promise f v2)
+
+val join_promise (#f:vprop) (v1:vprop) (v2:vprop)
+  : stt unit (promise f v1 ** promise f v2)
+             (fun () -> promise f (v1 ** v2))
+
+val split_promise (#f:vprop) (v1:vprop) (v2:vprop)
+  : stt unit (promise f (v1 ** v2))
+             (fun () -> promise f v1 ** promise f v2)
+
+// TODO: write a variant that assumes f too
+val rewrite_promise (#f:vprop) (v1 : vprop) (v2 : vprop)
+  (k : unit -> stt unit v1 (fun _ -> v2))
+  : stt unit (promise f v1)
+             (fun _ -> promise f v2)
diff --git a/share/steel/examples/pulse/parix/TaskPool.Examples.fst b/share/steel/examples/pulse/parix/TaskPool.Examples.fst
new file mode 100644
index 000000000..c5926ecdf
--- /dev/null
+++ b/share/steel/examples/pulse/parix/TaskPool.Examples.fst
@@ -0,0 +1,124 @@
+module TaskPool.Examples
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Par.Pledge
+open TaskPool
+
+assume
+val qsv : nat -> vprop
+assume
+val qsc : n:nat -> stt unit emp (fun _ -> qsv n)
+
+let spawn_ #pre #post p f = spawn_ #full_perm #pre #post p f
+
+```pulse
+fn qs (n:nat)
+  requires emp
+  returns _:unit
+  ensures qsv 1 ** qsv 2 ** qsv 3 ** qsv 4
+{
+  let p = setup_pool 42;
+  spawn_ p (fun () -> qsc 1);
+  spawn_ p (fun () -> qsc 2);
+  spawn_ p (fun () -> qsc 3);
+  spawn_ p (fun () -> qsc 4);
+  teardown_pool p;
+  redeem_pledge emp_inames (pool_done p) (qsv 1);
+  redeem_pledge emp_inames (pool_done p) (qsv 2);
+  redeem_pledge emp_inames (pool_done p) (qsv 3);
+  redeem_pledge emp_inames (pool_done p) (qsv 4);
+  drop_ (pool_done p);
+  ()
+}
+```
+
+```pulse
+fn qs_joinpromises (n:nat)
+  requires emp
+  returns _:unit
+  ensures qsv 1 ** qsv 2 ** qsv 3 ** qsv 4
+{
+  let p = setup_pool 42;
+  spawn_ p (fun () -> qsc 1);
+  spawn_ p (fun () -> qsc 2);
+  spawn_ p (fun () -> qsc 3);
+  spawn_ p (fun () -> qsc 4);
+  join_pledge #emp_inames #(pool_done p) (qsv 1) (qsv 2);
+  join_pledge #emp_inames #(pool_done p) (qsv 3) (qsv 4);
+  teardown_pool p;
+  redeem_pledge emp_inames (pool_done p) (qsv 1 ** qsv 2);
+  redeem_pledge emp_inames (pool_done p) (qsv 3 ** qsv 4);
+  drop_ (pool_done p);
+  ()
+}
+```
+
+```pulse
+fn qs12 (_:unit)
+  requires emp
+  returns _:unit
+  ensures qsv 1 ** qsv 2
+  {
+    qsc 1;
+    qsc 2
+  }
+```
+
+```pulse
+fn qsh (n:nat)
+  requires emp
+  returns _:unit
+  ensures qsv 1 ** qsv 2 ** qsv 3 ** qsv 4
+{
+  let p = setup_pool 42;
+  spawn_ p qs12;
+  // could do the same thing for 3&4... it's gonna work.
+  // also qs12 could spawn and join its tasks, it would clearly work
+  spawn_ p (fun () -> qsc 3);
+  spawn_ p (fun () -> qsc 4);
+  teardown_pool p;
+  redeem_pledge emp_inames (pool_done p) (qsv 1 ** qsv 2);
+  redeem_pledge emp_inames (pool_done p) (qsv 3);
+  redeem_pledge emp_inames (pool_done p) (qsv 4);
+  drop_ (pool_done p);
+  ()
+}
+```
+
+```pulse
+fn qs12_par (p:pool)
+  requires pool_alive p
+  returns _:unit
+  ensures pool_alive p ** pledge emp_inames (pool_done p) (qsv 1) ** pledge emp_inames (pool_done p) (qsv 2)
+  {
+    spawn_ p (fun () -> qsc 1);
+    spawn_ p (fun () -> qsc 2);
+    ()
+  }
+```
+
+[@@expect_failure]
+```pulse
+fn qsh_par (n:nat)
+  requires emp
+  returns _:unit
+  ensures qsv 1 ** qsv 2 ** qsv 3 ** qsv 4
+{
+  let p = setup_pool 42;
+  spawn p (fun () -> qs12_par p);
+  (* Ah! This cannot work right now since we need to share part
+  of the pool_alive vprop to the spawned task, so we have
+  to index pool_alive with a permission, and allow
+  share/gather. *)
+  
+  spawn p (fun () -> qsc 3);
+  spawn p (fun () -> qsc 4);
+  teardown_pool p;
+  redeem_pledge (pool_done p) (qsv 1)
+  redeem_pledge (pool_done p) (qsv 2);
+  redeem_pledge (pool_done p) (qsv 3);
+  redeem_pledge (pool_done p) (qsv 4);
+  drop_ (pool_done p);
+  ()
+}
+```
diff --git a/share/steel/examples/pulse/parix/TaskPool.fst b/share/steel/examples/pulse/parix/TaskPool.fst
new file mode 100644
index 000000000..320195f7d
--- /dev/null
+++ b/share/steel/examples/pulse/parix/TaskPool.fst
@@ -0,0 +1,72 @@
+module TaskPool
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.SpinLock
+open Pulse.Lib.Par.Pledge
+
+module T = FStar.Tactics.V2
+
+let pool : Type0 = magic ()
+let pool_alive (#[T.exact (`full_perm)]p : perm) (pool:pool) : vprop
+  = magic()
+let pool_done = magic ()
+
+let setup_pool (n:nat)
+  = magic ()
+
+let task_handle pool a post = magic ()
+let joinable #p #a #post th = magic ()
+let joined   #p #a #post th = magic ()
+
+let handle_solved #p #a #post th = magic()
+
+let spawn #a #pre #post #e = magic ()
+
+let spawn_ #pre #post #e = magic ()
+
+let must_be_done = magic ()
+
+let join0 = magic ()
+
+#set-options "--print_universes"
+
+#set-options "--print_universes"
+
+```pulse
+fn __extract
+  (#p:pool)
+  (#a:Type0)
+  (#post : (a -> vprop))
+  (th : task_handle p a post)
+  requires handle_solved th
+  returns x:a
+  ensures post x
+{
+  admit()
+}
+``` 
+
+let extract = __extract
+
+let split_alive _ _ = admit()
+
+```pulse
+fn __join
+  (#p:pool)
+  (#a:Type0)
+  (#post : (a -> vprop))
+  (th : task_handle p a post)
+  requires joinable th
+  returns x:a
+  ensures post x
+{
+  join0 th;
+  extract th
+}
+``` 
+let join = __join
+
+let teardown_pool
+  (p:pool)
+  : stt unit (pool_alive p) (fun _ -> pool_done p)
+  = magic ()
diff --git a/share/steel/examples/pulse/parix/TaskPool.fsti b/share/steel/examples/pulse/parix/TaskPool.fsti
new file mode 100644
index 000000000..9bcb8c3dd
--- /dev/null
+++ b/share/steel/examples/pulse/parix/TaskPool.fsti
@@ -0,0 +1,89 @@
+module TaskPool
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.SpinLock
+open Pulse.Lib.Par.Pledge
+module T = FStar.Tactics
+
+val pool : Type0
+val pool_alive : (#[T.exact (`full_perm)]p : perm) -> pool -> vprop
+val pool_done : pool -> vprop
+
+val setup_pool (n:nat)
+  : stt pool emp (fun p -> pool_alive #full_perm p)
+
+val task_handle : pool -> a:Type0 -> (a -> vprop) -> Type0
+val joinable : #p:pool -> #a:Type0 -> #post:_ -> th:(task_handle p a post) -> vprop
+val joined   : #p:pool -> #a:Type0 -> #post:_ -> th:(task_handle p a post) -> vprop
+
+val handle_solved
+  (#p : pool) 
+  (#a : Type0)
+  (#post : a -> vprop)
+  (th : task_handle p a post)
+  : vprop
+
+(* NOTE! Spawn only requires an *epsilon* of permission over the pool.
+We do not have to be exclusive owners of it in order to queue a job,
+even if that modifies it. How to model this under the hood? *)
+val spawn
+  (#a : Type0)
+  (#pre : vprop) (#post : a -> vprop)
+  (#[T.exact (`full_perm)]e : perm)
+  (p:pool)
+  ($f : unit -> stt a pre (fun (x:a) -> post x))
+  : stt (task_handle p a post)
+        (pool_alive #e p ** pre)
+        (fun th -> pool_alive #e p ** joinable th ** pledge emp_inames (joined th) (handle_solved th))
+
+(* Spawn of a unit-returning task with no intention to join, simpler. *)
+val spawn_
+  (#[T.exact (`full_perm)]e : perm)
+  (#pre #post : _)
+  (p:pool) (f : unit -> stt unit pre (fun _ -> post))
+  : stt unit (pool_alive #e p ** pre)
+             (fun prom -> pool_alive #e p ** pledge emp_inames (pool_done p) post)
+
+(* If the pool is done, all pending joinable threads must be done *)
+val must_be_done
+  (#p : pool)
+  (#a: Type0)
+  (#post : a -> vprop)
+  (th : task_handle p a post)
+  : stt_ghost unit emp_inames (pool_done p ** joinable th) (fun () -> pool_done p ** handle_solved th)
+
+val join0
+  (#p:pool)
+  (#a:Type0)
+  (#post : a -> vprop)
+  (th : task_handle p a post)
+  : stt unit (joinable th) (fun () -> handle_solved th)
+
+val extract
+  (#p:pool)
+  (#a:Type0)
+  (#post : a -> vprop)
+  (th : task_handle p a post)
+  : stt a (handle_solved th) (fun x -> post x)
+  
+val split_alive
+  (p:pool)
+  (e:perm)
+  : stt_ghost unit emp_inames
+              (pool_alive #e p)
+              (fun () -> pool_alive #(half_perm e) p ** pool_alive #(half_perm e) p)
+
+val join
+  (#p:pool)
+  (#a:Type0)
+  (#post : a -> vprop)
+  (th : task_handle p a post)
+  : stt a (joinable th) (fun x -> post x)
+// let join =
+//   bind_stt (join0 th) (fun () ->
+//   extract th)
+
+(* We must exclusively own the pool in order to terminate it. *)
+val teardown_pool
+  (p:pool)
+  : stt unit (pool_alive #full_perm p) (fun _ -> pool_done p)
diff --git a/share/steel/examples/pulse/parix/UnixFork.fsti b/share/steel/examples/pulse/parix/UnixFork.fsti
new file mode 100644
index 000000000..377cf2308
--- /dev/null
+++ b/share/steel/examples/pulse/parix/UnixFork.fsti
@@ -0,0 +1,21 @@
+module UnixFork
+
+(* This module assumes an unstructured unix-style fork *)
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Par.Pledge
+
+new
+val thread : Type0
+
+val joinable : thread -> vprop
+val done     : thread -> vprop (* i.e. reapable/zombie *)
+
+val fork 
+  (#pre #post : vprop)
+  (f : unit -> stt unit pre (fun () -> post))
+  : stt thread pre (fun th -> joinable th ** pledge emp_inames (done th) post)
+
+val join
+  (th : thread)
+  : stt unit (joinable th) (fun () -> done th)