diff --git a/lib/common/Pulse.Lib.Core.Inv.fsti b/lib/common/Pulse.Lib.Core.Inv.fsti
new file mode 100644
index 000000000..744372ae8
--- /dev/null
+++ b/lib/common/Pulse.Lib.Core.Inv.fsti
@@ -0,0 +1,64 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.Core.Inv
+open Pulse.Lib.Core
+open FStar.Ghost
+open PulseCore.FractionalPermission
+open PulseCore.Observability
+open FStar.PCM
+open FStar.ExtractAs
+module T = FStar.Tactics.V2
+
+val inv (i:iname) (p:slprop) : slprop
+
+instance val placeless_inv (i: iname) (p: slprop) : placeless (inv i p)
+
+val dup_inv (i:iname) (p:slprop)
+  : stt_ghost unit emp_inames (inv i p) (fun _ -> inv i p ** inv i p)
+
+val fresh_invariant
+    (ctx:inames { Pulse.Lib.GhostSet.is_finite ctx })
+    (p:slprop)
+    {| placeless p |}
+: stt_ghost (i:iname { ~(i `GhostSet.mem` ctx) }) emp_inames p (fun i -> inv i p)
+
+inline_for_extraction [@@extract_as
+    (`(fun (#a:Type0) (#obs #fp #fp' #f_opens #p i:unit) (f:unit -> Dv a) ->
+        f ()))]
+val with_invariant
+    (#a:Type u#a)
+    (#obs:_)
+    (#fp:slprop)
+    (#fp':a -> slprop)
+    (#f_opens:inames)
+    (#p:slprop)
+    (i:iname { not (mem_inv f_opens i) })
+    ($f:unit -> stt_atomic a #obs f_opens
+                           (later p ** fp)
+                           (fun x -> later p ** fp' x))
+: stt_atomic a #obs (add_inv f_opens i) (inv i p ** fp) (fun x -> inv i p ** fp' x)
+
+[@@allow_ambiguous]
+val invariant_name_identifies_invariant
+      (#p #q:slprop)
+      (i:iname)
+      (j:iname { i == j } )
+: stt_ghost
+    unit
+    emp_inames
+    (inv i p ** inv j q)
+    (fun _ -> inv i p ** inv j q ** later (equiv p q))
diff --git a/lib/common/Pulse.Lib.Core.Refs.fsti b/lib/common/Pulse.Lib.Core.Refs.fsti
index f61a5f232..045ca6889 100644
--- a/lib/common/Pulse.Lib.Core.Refs.fsti
+++ b/lib/common/Pulse.Lib.Core.Refs.fsti
@@ -56,6 +56,8 @@ val timeless_pcm_pts_to
 : Lemma (timeless (pcm_pts_to r v))
         [SMTPat (timeless (pcm_pts_to r v))]
 
+instance val placeless_pcm_pts_to #a #p r v : placeless (pcm_pts_to #a #p r v)
+
 let pcm_ref_null
     (#a:Type)
     (p:FStar.PCM.pcm a)
@@ -159,6 +161,9 @@ val timeless_ghost_pcm_pts_to
 : Lemma (timeless (ghost_pcm_pts_to r v))
         [SMTPat (timeless (ghost_pcm_pts_to r v))]
 
+instance val placeless_ghost_pcm_pts_to #a #p r v :
+    placeless (ghost_pcm_pts_to #a #p r v)
+
 val ghost_pts_to_not_null
     (#a:Type)
     (#p:pcm a)
diff --git a/lib/common/Pulse.Lib.Core.fsti b/lib/common/Pulse.Lib.Core.fsti
index fe6b57a68..be0488c7a 100644
--- a/lib/common/Pulse.Lib.Core.fsti
+++ b/lib/common/Pulse.Lib.Core.fsti
@@ -175,8 +175,6 @@ let inames_subset (is1 is2 : inames) : Type0 =
 let (/!) (is1 is2 : inames) : Type0 =
   GhostSet.disjoint is1 is2
 
-val inv (i:iname) (p:slprop) : slprop
-
 let mem_iname (e:inames) (i:iname) : erased bool = elift2 (fun e i -> GhostSet.mem i e) e i
 let mem_inv (e:inames) (i:iname) : GTot bool = mem_iname e i
 
@@ -226,11 +224,6 @@ val frame_stt
   (e:stt a pre post)
 : stt a (pre ** frame) (fun x -> post x ** frame)
 
-val fork
-  (#pre:slprop)
-  (f:unit -> stt unit pre (fun _ -> emp))
-: stt unit pre (fun _ -> emp)
-
 val sub_stt (#a:Type u#a)
             (#pre1:slprop)
             (pre2:slprop)
@@ -441,12 +434,61 @@ val sub_invs_ghost
     (_ : squash (inames_subset opens1 opens2))
 : stt_ghost a opens2 pre post
 
+////////////////////////////////////////////////////////////////////
+// Locations
+////////////////////////////////////////////////////////////////////
+
+[@@erasable] val loc_id : Type0
+
+val process_of : loc_id -> loc_id
+val process_of_idem (l:loc_id) : Lemma (process_of (process_of l) == process_of l)
+  [SMTPat (process_of (process_of l))]
+
+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 -> 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)
+val loc_gather l #l' : stt_ghost unit emp_inames (loc l ** loc l') (fun _ -> loc l ** pure (l == l'))
+
+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)
+
+instance val placeless_emp : placeless emp
+instance val placeless_star (a b: slprop) {| placeless a, placeless b |} : placeless (a ** b)
+instance val placeless_pure (p: prop) : placeless (pure p)
+instance val placeless_exists #a (p: a -> slprop) {| ((x:a) -> placeless (p x)) |} :
+  placeless (op_exists_Star p)
+instance val placeless_on (l: loc_id) (p: slprop) : placeless (on l p)
+
+val ghost_impersonate
+  (#[T.exact (`emp_inames)] is: inames)
+  (l: loc_id) (pre post: slprop) {| placeless pre, placeless post |}
+  (f: unit -> stt_ghost unit is (loc l ** pre) (fun _ -> loc l ** post))
+  : stt_ghost unit is pre (fun _ -> post)
+
 //////////////////////////////////////////////////////////////////////////
 // Later
 //////////////////////////////////////////////////////////////////////////
 
 val later_credit (amt: nat) : slprop
 
+instance val placeless_later_credit amt : placeless (later_credit amt)
+
 val timeless_later_credit (amt: nat)
 : Lemma (timeless (later_credit amt))
         [SMTPat (timeless (later_credit amt))]
@@ -471,6 +513,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
 //////////////////////////////////////////////////////////////////////////
@@ -478,6 +523,8 @@ val exists_later (#t: Type) (f:t->slprop) : stt_ghost unit emp_inames (exists* x
 (* Two slprops are equal when approximated to the current heap level. *)
 val equiv (a b: slprop) : slprop
 
+instance val placeless_equiv a b : placeless (equiv a b)
+
 val equiv_dup a b : stt_ghost unit emp_inames (equiv a b) fun _ -> equiv a b ** equiv a b
 val equiv_refl a : stt_ghost unit emp_inames emp fun _ -> equiv a a
 val equiv_comm a b : stt_ghost unit emp_inames (equiv a b) fun _ -> equiv b a
@@ -502,6 +549,8 @@ val null_slprop_ref : slprop_ref
 
 val slprop_ref_pts_to ([@@@mkey]x: slprop_ref) (y: slprop) : slprop
 
+instance val placeless_slprop_ref_pts_to x y : placeless (slprop_ref_pts_to x y)
+
 val slprop_ref_alloc (y: slprop)
 : stt_ghost slprop_ref emp_inames emp fun x -> slprop_ref_pts_to x y
 
@@ -512,57 +561,6 @@ val slprop_ref_share (x: slprop_ref) (#y: slprop)
 val slprop_ref_gather (x: slprop_ref) (#y1 #y2: slprop)
 : stt_ghost unit emp_inames (slprop_ref_pts_to x y1 ** slprop_ref_pts_to x y2) fun _ -> slprop_ref_pts_to x y1 ** later (equiv y1 y2)
 
-//////////////////////////////////////////////////////////////////////////
-// Invariants
-//////////////////////////////////////////////////////////////////////////
-
-val dup_inv (i:iname) (p:slprop)
-  : stt_ghost unit emp_inames (inv i p) (fun _ -> inv i p ** inv i p)
-
-val new_invariant (p:slprop)
-: stt_ghost iname emp_inames p (fun i -> inv i p)
-
-val fresh_invariant
-    (ctx:inames { Pulse.Lib.GhostSet.is_finite ctx })
-    (p:slprop)
-: stt_ghost (i:iname { ~(i `GhostSet.mem` ctx) }) emp_inames p (fun i -> inv i p)
-
-val with_invariant
-    (#a:Type)
-    (#obs:_)
-    (#fp:slprop)
-    (#fp':a -> slprop)
-    (#f_opens:inames)
-    (#p:slprop)
-    (i:iname { not (mem_inv f_opens i) })
-    ($f:unit -> stt_atomic a #obs f_opens
-                           (later p ** fp)
-                           (fun x -> later p ** fp' x))
-: stt_atomic a #obs (add_inv f_opens i) (inv i p ** fp) (fun x -> inv i p ** fp' x)
-
-val with_invariant_g
-    (#a:Type)
-    (#fp:slprop)
-    (#fp':a -> slprop)
-    (#f_opens:inames)
-    (#p:slprop)
-    (i:iname { not (mem_inv f_opens i) })
-    ($f:unit -> stt_ghost a f_opens
-                            (later p ** fp)
-                            (fun x -> later p ** fp' x))
-: stt_ghost a (add_inv f_opens i) (inv i p ** fp) (fun x -> inv i p ** fp' x)
-
-[@@allow_ambiguous]
-val invariant_name_identifies_invariant
-      (#p #q:slprop)
-      (i:iname)
-      (j:iname { i == j } )
-: stt_ghost
-    unit
-    emp_inames
-    (inv i p ** inv j q)
-    (fun _ -> inv i p ** inv j q ** later (equiv p q))
-
 (***** end computation types and combinators *****)
 
 (* This tactic is called to find non_informative witnesses.
@@ -575,6 +573,11 @@ let non_info_tac () : T.Tac unit =
 // Some basic actions and ghost operations
 //////////////////////////////////////////////////////////////////////////
 
+val fork
+  (pre:slprop) {| placeless pre |} #l
+  (f: (l':loc_id { process_of l' == process_of l } -> stt unit (loc l' ** pre) (fun _ -> emp)))
+: stt unit (loc l ** pre) (fun _ -> emp)
+
 val rewrite (p:slprop) (q:slprop) (_:slprop_equiv p q)
 : stt_ghost unit emp_inames p (fun _ -> q)
 
diff --git a/lib/core/Pulse.Lib.Core.Inv.fst b/lib/core/Pulse.Lib.Core.Inv.fst
new file mode 100644
index 000000000..3ed2397da
--- /dev/null
+++ b/lib/core/Pulse.Lib.Core.Inv.fst
@@ -0,0 +1,40 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module Pulse.Lib.Core.Inv
+module I = PulseCore.InstantiatedSemantics
+module A = PulseCore.Atomic
+module T = FStar.Tactics.V2
+open PulseCore.InstantiatedSemantics
+open PulseCore.FractionalPermission
+open PulseCore.Observability
+friend PulseCore.InstantiatedSemantics
+friend Pulse.Lib.Core
+module Sep = PulseCore.IndirectionTheorySep
+
+(* Invariants, just reexport *)
+module Act = PulseCore.Action
+
+let inv i p = Act.(inv i p)
+
+let placeless_inv _ _ = admit ()
+
+////////////////////////////////////////////////////////////////////
+// Invariants
+////////////////////////////////////////////////////////////////////
+let dup_inv = A.dup_inv
+let fresh_invariant i p #_ = A.fresh_invariant i p
+let with_invariant = A.with_invariant
+let invariant_name_identifies_invariant #p #q i j = A.invariant_name_identifies_invariant p q i j
diff --git a/lib/core/Pulse.Lib.Core.Refs.fst b/lib/core/Pulse.Lib.Core.Refs.fst
index 1051b6ac6..031014981 100644
--- a/lib/core/Pulse.Lib.Core.Refs.fst
+++ b/lib/core/Pulse.Lib.Core.Refs.fst
@@ -35,6 +35,7 @@ let is_null_core_pcm_ref r = PulseCore.Action.is_core_ref_null r
 let pcm_pts_to #a (#p:pcm a) (r:pcm_ref p) (v:a) =
   PulseCore.Action.pts_to #a #p r v
 let timeless_pcm_pts_to #a #p r v = PulseCore.Action.timeless_pts_to #a #p r v
+let placeless_pcm_pts_to #a #p r v = admit ()
 let pts_to_not_null #a #p r v = A.pts_to_not_null #a #p r v
 
 let alloc
@@ -82,6 +83,7 @@ let null_core_ghost_pcm_ref = PulseCore.Action.core_ghost_ref_null
 
 let ghost_pcm_pts_to #a #p r v = PulseCore.Action.ghost_pts_to #a #p r v
 let timeless_ghost_pcm_pts_to #a #p r v = PulseCore.Action.timeless_ghost_pts_to #a #p r v
+let placeless_ghost_pcm_pts_to #a #p r v = admit ()
 let ghost_pts_to_not_null #a #p r v = A.ghost_pts_to_not_null #a #p r v
 let ghost_alloc = A.ghost_alloc
 let ghost_read = A.ghost_read
diff --git a/lib/core/Pulse.Lib.Core.fst b/lib/core/Pulse.Lib.Core.fst
index 68b461d16..2489fc337 100644
--- a/lib/core/Pulse.Lib.Core.fst
+++ b/lib/core/Pulse.Lib.Core.fst
@@ -139,8 +139,6 @@ let join_emp is =
   GhostSet.lemma_equal_intro (join_inames is emp_inames) is;
   GhostSet.lemma_equal_intro (join_inames emp_inames is) is
 
-let inv i p = Act.(inv i p)
-let inames_live = Sep.inames_live
 let add_already_there i is = GhostSet.lemma_equal_intro (add_inv is i) is
 
 ////////////////////////////////////////////////////////////////////
@@ -150,7 +148,6 @@ let stt = I.stt
 let return_stt_noeq = I.return
 let bind_stt = I.bind
 let frame_stt = I.frame
-let fork f = I.fork (f ())
 let sub_stt = I.sub
 let conv_stt pf1 pf2 = I.conv #_ _ _ _ _ pf1 pf2
 let hide_div = I.hide_div
@@ -181,11 +178,39 @@ let frame_ghost = A.frame_ghost
 let sub_ghost = A.sub_ghost
 let sub_invs_ghost = A.sub_invs_stt_ghost
 
+////////////////////////////////////////////////////////////////////
+// Locations
+////////////////////////////////////////////////////////////////////
+
+let loc_id = unit
+let process_of = id
+let process_of_idem l = ()
+let loc l = emp
+let loc_get () = admit ()
+let loc_dup l = admit ()
+let loc_gather l = admit ()
+
+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 ()
+let placeless_exists _ = admit ()
+let placeless_on _ _ = admit ()
+let placeless_inv _ _ = admit ()
+
+let ghost_impersonate l pre post f = admit ()
+
 //////////////////////////////////////////////////////////////////////////
 // Later
 //////////////////////////////////////////////////////////////////////////
 
 let later_credit = later_credit
+let placeless_later_credit amt = admit ()
 let timeless_later_credit amt = Sep.timeless_later_credit amt
 let later_credit_zero _ = PulseCore.InstantiatedSemantics.later_credit_zero ()
 let later_credit_add a b = PulseCore.InstantiatedSemantics.later_credit_add a b
@@ -216,6 +241,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
 //////////////////////////////////////////////////////////////////////////
@@ -224,6 +252,7 @@ let rewrite_eq p q (pf:squash (p == q))
   = slprop_equiv_elim p q;
     A.noop q
 let equiv = I.equiv
+let placeless_equiv a b = admit ()
 let equiv_dup a b = A.equiv_dup a b
 let equiv_refl a = A.equiv_refl a
 let equiv_comm a b = rewrite_eq (equiv a b) (equiv b a) (Sep.equiv_comm a b)
@@ -241,28 +270,17 @@ let later_equiv = Sep.later_equiv
 let slprop_ref = PulseCore.Action.slprop_ref
 let null_slprop_ref = PulseCore.Action.null_slprop_ref
 let slprop_ref_pts_to x y = PulseCore.Action.slprop_ref_pts_to x y
+let placeless_slprop_ref_pts_to = admit ()
 let slprop_ref_alloc x = A.slprop_ref_alloc x
 let slprop_ref_share x #y = A.slprop_ref_share x y
 let slprop_ref_gather x #y1 #y2 = A.slprop_ref_gather x y1 y2
 
-////////////////////////////////////////////////////////////////////
-// Invariants
-////////////////////////////////////////////////////////////////////
-let dup_inv = A.dup_inv
-let new_invariant = A.new_invariant
-let fresh_invariant = A.fresh_invariant
-let inames_live_inv = A.inames_live_inv
-let inames_live_empty _ = rewrite_eq emp (inames_live emp_inames) (Sep.inames_live_empty ())
-let share_inames_live i j = rewrite_eq (inames_live (GhostSet.union i j)) (inames_live i ** inames_live j) (Sep.inames_live_union i j)
-let gather_inames_live i j = rewrite_eq (inames_live i ** inames_live j) (inames_live (GhostSet.union i j)) (Sep.inames_live_union i j)
-let with_invariant = A.with_invariant
-let with_invariant_g = A.with_invariant_g
-let invariant_name_identifies_invariant #p #q i j = A.invariant_name_identifies_invariant p q i j
-
 //////////////////////////////////////////////////////////////////////////
 // Some basic actions and ghost operations
 //////////////////////////////////////////////////////////////////////////
 
+let fork pre #_ #l f = I.fork (f l)
+
 let rewrite p q (pf:slprop_equiv p q)
   : stt_ghost unit emp_inames p (fun _ -> q)
   = slprop_equiv_elim p q;
diff --git a/lib/pulse/lib/Pulse.Lib.AnchoredReference.fst b/lib/pulse/lib/Pulse.Lib.AnchoredReference.fst
index ac33c93dd..717d50bb6 100644
--- a/lib/pulse/lib/Pulse.Lib.AnchoredReference.fst
+++ b/lib/pulse/lib/Pulse.Lib.AnchoredReference.fst
@@ -58,6 +58,8 @@ let pts_to_full
 : p:slprop { timeless p }
 = core_pts_to r #q n true
 
+let placeless_pts_to_full r n = Tactics.Typeclasses.solve
+
 let pts_to
   (#a:Type) (#p:preorder a) (#anc:anchor_rel p)
   (r:ref a p anc)
@@ -66,6 +68,8 @@ let pts_to
 : p:slprop { timeless p }
 = core_pts_to r #q n false
 
+let placeless_pts_to r n = Tactics.Typeclasses.solve
+
 let anchored
   (#a:Type)
   (#p:_)
@@ -77,12 +81,16 @@ let anchored
     GPR.pts_to r k **
     pure (owns_only_anchor n k)
 
+let placeless_anchored r n = Tactics.Typeclasses.solve
+
 let snapshot (#a:Type) (#p:_) (#anc:_) (r : ref a p anc) (n:a)
 : p:slprop { timeless p }
 = exists* (k:FRAP.knowledge anc) .
     GPR.pts_to r k **
     pure (snapshot_pred n k)
 
+let placeless_snapshot r n = Tactics.Typeclasses.solve
+
 let init_val (#a:Type) (#p:_) (anc:anchor_rel p) (x:a { anc x x })
 : v:FRAP.knowledge anc { fractional_ownership_maybe_with_anchor 1.0R x true true v }
 = let perm = (Some 1.0R, (Some x)) in
diff --git a/lib/pulse/lib/Pulse.Lib.AnchoredReference.fsti b/lib/pulse/lib/Pulse.Lib.AnchoredReference.fsti
index 74cb9063e..ec9d5c531 100644
--- a/lib/pulse/lib/Pulse.Lib.AnchoredReference.fsti
+++ b/lib/pulse/lib/Pulse.Lib.AnchoredReference.fsti
@@ -37,6 +37,9 @@ val pts_to_full
   (n:a)
 : p:slprop { timeless p }
 
+instance val placeless_pts_to_full #a #p #anc r #pr n :
+  placeless (pts_to_full #a #p #anc r #pr n)
+
 val pts_to
   (#a:Type) (#p:_) (#anc:_)
   ([@@@mkey]r:ref a p anc)
@@ -44,6 +47,9 @@ val pts_to
   (n:a)
 : p:slprop { timeless p }
 
+instance val placeless_pts_to #a #p #anc r #pr n :
+  placeless (pts_to #a #p #anc r #pr n)
+
 val anchored
   (#a:Type)
   (#p:_)
@@ -52,9 +58,14 @@ val anchored
   (n:a)
 : p:slprop{ timeless p }
 
+instance val placeless_anchored #a #p #anc r n :
+  placeless (anchored #a #p #anc r n)
+
 val snapshot (#a:Type) (#p:_) (#anc:_) (r : ref a p anc) (v:a)
 : p:slprop { timeless p }
 
+instance val placeless_snapshot #a #p #anc r n :
+  placeless (snapshot #a #p #anc r n)
 
 ghost
 fn alloc (#a:Type) (x:a) (#p:_) (#anc:anchor_rel p)
diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst
index ab04fc191..e8d30598d 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.Core.fst
+++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fst
@@ -17,7 +17,6 @@
 module Pulse.Lib.Array.Core
 #lang-pulse
 open Pulse.Main
-open FStar.Tactics.V2
 open Pulse.Lib.Core
 open PulseCore.FractionalPermission
 open FStar.Ghost
@@ -29,6 +28,7 @@ module PM = Pulse.Lib.PCM.Map
 open Pulse.Lib.PCM.Array
 module PA = Pulse.Lib.PCM.Array
 open Pulse.Lib.PCMReference
+open Pulse.Class.Duplicable
 
 
 /// An abstract type to represent a base array (whole allocation
@@ -64,28 +64,33 @@ let is_full_array (#elt: Type) (a: array elt) : Tot prop =
 let null #a : array a = null_array'
 let is_null a = is_null_core_pcm_ref a.base_ref
 
-let lptr_of #elt (a: array elt) : pcm_ref (PA.pcm elt a.base_len) =
+let pcm (elt: Type) (len: erased nat) =
+  PA.pcm (elt & loc_id) len
+
+let lptr_of #elt (a: array elt) : pcm_ref (pcm elt a.base_len) =
   a.base_ref
 
 [@@noextract_to "krml"]
-let mk_carrier_f #elt (off: nat) (len: nat) (f: perm) (v: Seq.seq elt) (mask: nat -> bool) :
-    index_t len -> Pulse.Lib.PCM.Fraction.fractional elt = fun i ->
+let mk_carrier_f #elt (off: nat) (len: nat) (f: perm) (v: Seq.seq elt) (mask: nat -> bool) (l: loc_id) :
+    index_t len -> Pulse.Lib.PCM.Fraction.fractional (elt & loc_id) = fun i ->
   if off <= i && i < off + Seq.length v && mask (i - off) then
-    Some (Seq.index v (i - off), f)
+    Some ((Seq.index v (i - off), l), f)
   else
     None
 
+let carrier elt len = carrier (elt & loc_id) len
+
 [@@noextract_to "krml"]
-let mk_carrier #elt (off: nat) (len: nat) (f: perm) (v: Seq.seq elt) (mask: nat -> bool) : carrier elt len =
-  Map.map_literal #(index_t len) #(Pulse.Lib.PCM.Fraction.fractional elt) (mk_carrier_f off len f v mask)
+let mk_carrier #elt (off: nat) (len: nat) (f: perm) (v: Seq.seq elt) (mask: nat -> bool) (l: loc_id) : carrier elt len =
+  Map.map_literal (mk_carrier_f off len f v mask l)
 
 irreducible let pull_mask (f: nat -> prop) (len: nat) : Ghost (nat -> bool) (requires True)
     (ensures fun res -> forall i. res i <==> i >= len \/ f i) =
   let s = Seq.init_ghost len fun i -> IndefiniteDescription.strong_excluded_middle (f i) in
   fun i -> if i < len then Seq.index s i else true
 
-let mk_carrier' #t (a: array t) (f: perm) (v: Seq.seq t) (mask: nat -> prop) : GTot (carrier t a.base_len) =
-  mk_carrier a.offset a.base_len f v (pull_mask mask a.length)
+let mk_carrier' #t (a: array t) (f: perm) (v: Seq.seq t) (mask: nat -> prop) (l: loc_id) : GTot (carrier t a.base_len) =
+  mk_carrier a.offset a.base_len f v (pull_mask mask a.length) l
 
 let mask_nonempty (mask: nat -> prop) (len: nat) : prop =
   exists i. mask i /\ i < len
@@ -95,10 +100,33 @@ let squash' (t: Type u#a) = squash t
 let intro_squash #t (x: t) : squash' t = ()
 
 let pts_to_mask #t ([@@@mkey] a: array t) (#[full_default()] f: perm) (v: erased (Seq.seq t)) (mask: nat -> prop) : slprop =
-  pcm_pts_to (lptr_of a) (mk_carrier' a f v mask) **
+  exists* l. loc l **
+  pcm_pts_to (lptr_of a) (mk_carrier' a f v mask (process_of l)) **
   pure (Seq.length v == reveal a.length /\ (mask_nonempty mask a.length ==> f <=. 1.0R) /\ squash' t)
 
-let pts_to_mask_timeless _ _ _ _ = ()
+ghost fn is_send_pts_to_mask' u#a (#t: Type u#a) a #f v mask : is_send (pts_to_mask #t a #f v mask) = l1 l2 {
+  ghost_impersonate l1 (on l1 (pts_to_mask a #f v mask)) (on l2 (pts_to_mask a #f v mask)) fn _ {
+    on_elim _;
+    unfold pts_to_mask;
+    loc_gather l1;
+    ghost_impersonate l2
+      (pcm_pts_to (lptr_of a) (mk_carrier' a f v mask (process_of l1)) **
+        pure (Seq.length v == reveal a.length /\ (mask_nonempty mask a.length ==> f <=. 1.0R) /\ squash' t))
+      (on l2 (pts_to_mask a #f v mask))
+      fn _ {
+        loc_dup l2;
+        fold pts_to_mask a #f v mask;
+        on_intro (pts_to_mask a #f v mask)
+      }
+  }
+}
+let is_send_pts_to_mask = is_send_pts_to_mask'
+
+let pts_to_mask_timeless #t a f v mask =
+  assert_norm (pts_to_mask #t a #f v mask ==
+    exists* l. loc l **
+    pcm_pts_to (lptr_of a) (mk_carrier' a f v mask (process_of l)) **
+    pure (Seq.length v == reveal a.length /\ (mask_nonempty mask a.length ==> f <=. 1.0R) /\ squash' t))
 
 ghost
 fn pts_to_mask_props u#a (#t: Type u#a) (a:array t) (#p:perm) (#x:Seq.seq t) #mask
@@ -145,7 +173,8 @@ ghost fn mask_vext u#a (#t: Type u#a) (arr: array t) #f #v v' #mask
   ensures pts_to_mask arr #f v' mask
 {
   unfold pts_to_mask arr #f v mask;
-  assert pure (mk_carrier' arr f v mask `Map.equal` mk_carrier' arr f v' mask);
+  with l. assert loc l;
+  assert pure (mk_carrier' arr f v mask (process_of l) `Map.equal` mk_carrier' arr f v' mask (process_of l));
   fold pts_to_mask arr #f v' mask;
 }
 
@@ -155,7 +184,8 @@ ghost fn mask_mext u#a (#t: Type u#a) (arr: array t) #f #v #mask (mask': nat ->
   ensures pts_to_mask arr #f v mask'
 {
   unfold pts_to_mask arr #f v mask;
-  assert pure (mk_carrier' arr f v mask `Map.equal` mk_carrier' arr f v mask');
+  with l. assert loc l;
+  assert pure (mk_carrier' arr f v mask (process_of l) `Map.equal` mk_carrier' arr f v mask' (process_of l));
   fold pts_to_mask arr #f v mask';
 }
 
@@ -176,13 +206,14 @@ fn mask_alloc u#a (#elt: Type u#a) {| small_type u#a |} (x: elt) (n: SZ.t)
   ensures pts_to_mask a (Seq.create (SZ.v n) x) (fun _ -> True)
   ensures pure (length a == SZ.v n /\ is_full_array a)
 {
-  let v = mk_carrier 0 (SZ.v n) 1.0R (Seq.create (SZ.v n) x) (fun _ -> true);
-  FStar.PCM.compatible_refl (PA.pcm elt (SZ.v n)) v;
-  let b = alloc #_ #(PA.pcm elt (SZ.v n)) v;
+  loc_get (); with l. assert loc l;
+  let v = mk_carrier 0 (SZ.v n) 1.0R (Seq.create (SZ.v n) x) (fun _ -> true) (process_of l);
+  FStar.PCM.compatible_refl (pcm elt (SZ.v n)) v;
+  let b = alloc #_ #(pcm elt (SZ.v n)) v;
   pts_to_not_null b _;
   let arr: array elt = { base_ref = b; base_len = SZ.v n; length = SZ.v n; offset = 0 };
   rewrite each b as lptr_of arr;
-  assert pure (v `Map.equal` mk_carrier' arr 1.0R (Seq.create (SZ.v n) x) (fun _ -> l_True));
+  assert pure (v `Map.equal` mk_carrier' arr 1.0R (Seq.create (SZ.v n) x) (fun _ -> l_True) (process_of l));
   intro_squash x;
   fold pts_to_mask arr (Seq.create (SZ.v n) x) (fun _ -> l_True);
   arr
@@ -211,64 +242,70 @@ ghost fn pcm_rw u#a (#t: Type u#a)
     a1.base_len == a2.base_len /\
     a1.base_ref == a2.base_ref /\
     reveal a2.length == Seq.length s2 /\
-    mk_carrier' a1 p1 s1 m1 `Map.equal` mk_carrier' a2 p2 s2 m2
+    (forall l. mk_carrier' a1 p1 s1 m1 l `Map.equal` mk_carrier' a2 p2 s2 m2 l)
   )
   ensures pts_to_mask #t a2 #p2 s2 m2
 {
   unfold pts_to_mask a1 #p1 s1 m1;
+  with l. assert loc l;
   rewrite each lptr_of a1 as lptr_of a2;
   let i = get_mask_idx m2 (length a2);
   assert pure (mask_nonempty m2 (length a2) ==>
-    Map.sel (mk_carrier' a2 p2 s2 m2) (i + a2.offset) == Some (Seq.index s2 i, p2));
+    Map.sel (mk_carrier' a2 p2 s2 m2 (process_of l)) (i + a2.offset) == Some ((Seq.index s2 i, process_of l), p2));
   fold pts_to_mask a2 #p2 s2 m2;
 }
 
-ghost fn pcm_share u#a (#t: Type u#a)
+ghost fn pcm_share u#a (#t: Type u#a) #l
     (a: array t) p s m
     (a1: array t) p1 s1 m1
     (a2: array t) p2 s2 m2
+  preserves loc l
   requires pts_to_mask a #p s m
   requires pure (Seq.length s1 == a1.length)
   requires pure (Seq.length s2 == a2.length)
   requires pure (
     a1.base_len == a.base_len /\ a2.base_len == a.base_len /\
     a1.base_ref == a.base_ref /\ a2.base_ref == a.base_ref /\
-    composable (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2) /\
-    compose (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2)
-      `Map.equal` mk_carrier' a p s m
+    composable (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l)) /\
+    compose (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l))
+      `Map.equal` mk_carrier' a p s m (process_of l)
   )
   ensures pts_to_mask a1 #p1 s1 m1
   ensures pts_to_mask a2 #p2 s2 m2
 {
   unfold pts_to_mask a #p s m;
-  share (lptr_of a) (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2);
+  loc_gather l;
+  share (lptr_of a) (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l));
   rewrite
-    pcm_pts_to (lptr_of a) (mk_carrier' a1 p1 s1 m1) as
-    pcm_pts_to (lptr_of a1) (mk_carrier' a1 p1 s1 m1);
+    pcm_pts_to (lptr_of a) (mk_carrier' a1 p1 s1 m1 (process_of l)) as
+    pcm_pts_to (lptr_of a1) (mk_carrier' a1 p1 s1 m1 (process_of l));
   rewrite
-    pcm_pts_to (lptr_of a) (mk_carrier' a2 p2 s2 m2) as
-    pcm_pts_to (lptr_of a2) (mk_carrier' a2 p2 s2 m2);
+    pcm_pts_to (lptr_of a) (mk_carrier' a2 p2 s2 m2 (process_of l)) as
+    pcm_pts_to (lptr_of a2) (mk_carrier' a2 p2 s2 m2 (process_of l));
   let i1 = get_mask_idx m1 (length a1);
   let i2 = get_mask_idx m2 (length a2);
   assert pure (mask_nonempty m1 (length a1) ==>
-    Some? (Map.sel (mk_carrier' a p s m) (i1 + a1.offset)));
+    Some? (Map.sel (mk_carrier' a p s m (process_of l)) (i1 + a1.offset)));
+  loc_dup l;
   fold pts_to_mask a1 #p1 s1 m1;
   assert pure (mask_nonempty m2 (length a2) ==>
-    Some? (Map.sel (mk_carrier' a p s m) (i2 + a2.offset)));
+    Some? (Map.sel (mk_carrier' a p s m (process_of l)) (i2 + a2.offset)));
+  loc_dup l;
   fold pts_to_mask a2 #p2 s2 m2;
 }
 
-ghost fn pcm_gather u#a (#t: Type u#a)
+ghost fn pcm_gather u#a (#t: Type u#a) #l
     (a: array t) p s m
     (a1: array t) p1 s1 m1
     (a2: array t) p2 s2 m2
+  preserves loc l
   requires pure (Seq.length s == a.length)
   requires pure (
     a1.base_len == a.base_len /\ a2.base_len == a.base_len /\
     a1.base_ref == a.base_ref /\ a2.base_ref == a.base_ref /\
-    (composable (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2) ==>
-    compose (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2)
-      `Map.equal` mk_carrier' a p s m)
+    (composable (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l)) ==>
+    compose (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l))
+      `Map.equal` mk_carrier' a p s m (process_of l))
   )
   requires pts_to_mask a1 #p1 s1 m1
   requires pts_to_mask a2 #p2 s2 m2
@@ -276,23 +313,26 @@ ghost fn pcm_gather u#a (#t: Type u#a)
   ensures pure (
     a1.base_len == a.base_len /\ a2.base_len == a.base_len /\
     a1.base_ref == a.base_ref /\ a2.base_ref == a.base_ref /\
-    composable (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2) /\
-    compose (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2)
-      `Map.equal` mk_carrier' a p s m
+    composable (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l)) /\
+    compose (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l))
+      `Map.equal` mk_carrier' a p s m (process_of l)
   )
 {
   unfold pts_to_mask a1 #p1 s1 m1;
+  loc_gather l;
   unfold pts_to_mask a2 #p2 s2 m2;
+  loc_gather l;
   rewrite
-    pcm_pts_to (lptr_of a1) (mk_carrier' a1 p1 s1 m1) as
-    pcm_pts_to (lptr_of a) (mk_carrier' a1 p1 s1 m1);
+    pcm_pts_to (lptr_of a1) (mk_carrier' a1 p1 s1 m1 (process_of l)) as
+    pcm_pts_to (lptr_of a) (mk_carrier' a1 p1 s1 m1 (process_of l));
   rewrite
-    pcm_pts_to (lptr_of a2) (mk_carrier' a2 p2 s2 m2) as
-    pcm_pts_to (lptr_of a) (mk_carrier' a2 p2 s2 m2);
-  gather (lptr_of a) (mk_carrier' a1 p1 s1 m1) (mk_carrier' a2 p2 s2 m2);
+    pcm_pts_to (lptr_of a2) (mk_carrier' a2 p2 s2 m2 (process_of l)) as
+    pcm_pts_to (lptr_of a) (mk_carrier' a2 p2 s2 m2 (process_of l));
+  gather (lptr_of a) (mk_carrier' a1 p1 s1 m1 (process_of l)) (mk_carrier' a2 p2 s2 m2 (process_of l));
   let i = get_mask_idx m (length a);
   assert pure (mask_nonempty m a.length ==>
-    Map.sel (mk_carrier' a p s m) (i + a.offset) == Some (Seq.index s i, p));
+    Map.sel (mk_carrier' a p s m (process_of l)) (i + a.offset) == Some ((Seq.index s i, process_of l), p));
+  loc_dup l;
   fold pts_to_mask a #p s m;
 }
 
@@ -302,11 +342,13 @@ fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
   ensures pts_to_mask arr #(p /. 2.0R) s mask
   ensures pts_to_mask arr #(p /. 2.0R) s mask
 {
+  loc_get ();
   pts_to_mask_props arr;
   pcm_share
     arr p s mask
     arr (p /. 2.0R) s mask
     arr (p /. 2.0R) s mask;
+  drop_ (loc _);
 }
 
 [@@allow_ambiguous]
@@ -318,6 +360,7 @@ ghost fn mask_gather u#a (#t: Type u#a) (arr: array t) #p1 #p2 #s1 #s2 #mask1 #m
     pure ((Seq.length v == Seq.length s1 /\ Seq.length v == Seq.length s2) /\
       (forall (i: nat). i < Seq.length v /\ mask1 i ==> Seq.index v i == Seq.index s1 i /\ Seq.index v i == Seq.index s2 i))
 {
+  loc_get (); with l. assert loc l;
   mask_mext arr #p2 #s2 mask1;
   pts_to_mask_props arr #p1 #s1 #mask1;
   pts_to_mask_props arr #p2 #s2 #mask1;
@@ -326,7 +369,9 @@ ghost fn mask_gather u#a (#t: Type u#a) (arr: array t) #p1 #p2 #s1 #s2 #mask1 #m
     arr p1 s1 mask1
     arr p2 s2 mask1;
   assert pure (forall (i: nat). (i < Seq.length s1 /\ mask1 i) ==>
-    Map.sel (mk_carrier' arr p1 s1 mask1) (i + arr.offset) == Some (Seq.index s1 i, p1));
+    Map.sel (mk_carrier' arr p1 s1 mask1 (process_of l)) (i + arr.offset) ==
+      Some ((Seq.index s1 i, process_of l), p1));
+  drop_ (loc l);
 }
 
 ghost fn split_mask u#a (#t: Type u#a) (arr: array t) #f #v #mask (pred: nat -> prop)
@@ -334,11 +379,13 @@ ghost fn split_mask u#a (#t: Type u#a) (arr: array t) #f #v #mask (pred: nat ->
   ensures pts_to_mask arr #f v (mask_isect mask pred)
   ensures pts_to_mask arr #f v (mask_diff mask pred)
 {
+  loc_get ();
   pts_to_mask_props arr;
   pcm_share
     arr f v mask
     arr f v (mask_isect mask pred)
     arr f v (mask_diff mask pred);
+  drop_ (loc _);
 }
 
 let mix #t (v1: Seq.seq t) (v2: Seq.seq t { Seq.length v1 == Seq.length v2 }) (mask: nat -> prop) :
@@ -361,6 +408,7 @@ ghost fn join_mask u#a (#t: Type u#a) (arr: array t) #f #v1 #v2 #mask1 #mask2
         (mask1 i ==> Seq.index v i == Seq.index v1 i) /\
         (mask2 i ==> Seq.index v i == Seq.index v2 i)))
 {
+  loc_get ();
   pts_to_mask_props arr #f #v1 #mask1;
   pts_to_mask_props arr #f #v2 #mask2;
   let v = mix v1 v2 mask1;
@@ -369,6 +417,7 @@ ghost fn join_mask u#a (#t: Type u#a) (arr: array t) #f #v1 #v2 #mask1 #mask2
     arr f v mask
     arr f v1 mask1
     arr f v2 mask2;
+  drop_ (loc _);
 }
 
 [@@allow_ambiguous]
@@ -392,11 +441,14 @@ fn pts_to_mask_injective_eq u#a (#a: Type u#a) #p0 #p1 #s0 #s1 #mask0 #mask1 (ar
       Seq.index s0 i == Seq.index s1 i))
 {
   unfold pts_to_mask arr #p0 s0 mask0;
+  with l. assert loc l;
   unfold pts_to_mask arr #p1 s1 mask1;
-  gather (lptr_of arr) (mk_carrier' arr p0 s0 mask0) (mk_carrier' arr p1 s1 mask1);
-  share (lptr_of arr) (mk_carrier' arr p0 s0 mask0) (mk_carrier' arr p1 s1 mask1);
+  loc_gather l;
+  gather (lptr_of arr) (mk_carrier' arr p0 s0 mask0 (process_of l)) (mk_carrier' arr p1 s1 mask1 (process_of l));
+  share (lptr_of arr) (mk_carrier' arr p0 s0 mask0 (process_of l)) (mk_carrier' arr p1 s1 mask1 (process_of l));
   assert pure (forall (i: nat). i < Seq.length s0 /\ mask0 i ==>
-    Map.sel (mk_carrier' arr p0 s0 mask0) (i + arr.offset) == Some (Seq.index s0 i, p0));
+    Map.sel (mk_carrier' arr p0 s0 mask0 (process_of l)) (i + arr.offset) == Some ((Seq.index s0 i, process_of l), p0));
+  loc_dup l;
   fold pts_to_mask arr #p0 s0 mask0;
   fold pts_to_mask arr #p1 s1 mask1;
 }
@@ -412,7 +464,7 @@ fn mask_read u#a (#t: Type u#a) (a: array t) (i: SZ.t) #p (#s: erased (Seq.seq t
   with w. assert pcm_pts_to (lptr_of a) w;
   let v = read (lptr_of a) w (fun _ -> w);
   fold pts_to_mask a #p s mask;
-  fst (Some?.v (FStar.Map.sel v (a.offset + SZ.v i)));
+  fst (fst (Some?.v (FStar.Map.sel v (a.offset + SZ.v i))));
 }
 
 [@@noextract_to "krml"]
@@ -422,19 +474,20 @@ fn mask_write u#a (#t: Type u#a) (a: array t) (i: SZ.t) (v: t) (#s: erased (Seq.
   ensures pts_to_mask a (Seq.upd s (SZ.v i) v) mask
 {
   unfold pts_to_mask a s mask;
+  with l. assert loc l;
   with w. assert (pcm_pts_to (lptr_of a) w);
   write (lptr_of a) w _
       (PM.lift_frame_preserving_upd
         _ _
         (Frac.mk_frame_preserving_upd
-          (Seq.index s (SZ.v i))
-          v
+          (Seq.index s (SZ.v i), process_of l)
+          (v, process_of l)
         )
         _ (a.offset + SZ.v i));
   assert pure (
-    Map.upd (mk_carrier' a 1.0R s mask) (a.offset + SZ.v i) (Some (v, 1.0R))
+    Map.upd (mk_carrier' a 1.0R s mask (process_of l)) (a.offset + SZ.v i) (Some ((v, process_of l), 1.0R))
     `Map.equal`
-    mk_carrier' a 1.0R (Seq.upd s (SZ.v i) v) mask
+    mk_carrier' a 1.0R (Seq.upd s (SZ.v i) v) mask (process_of l)
   );
   fold pts_to_mask a (Seq.upd s (SZ.v i) v) mask;
 }
diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti
index b06e81f05..ee8737d97 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti
@@ -16,7 +16,6 @@
 
 module Pulse.Lib.Array.Core
 #lang-pulse
-open FStar.Tactics.V2
 open Pulse.Lib.Core
 open Pulse.Main
 open Pulse.Class.PtsTo
@@ -24,6 +23,7 @@ open PulseCore.FractionalPermission
 open FStar.Ghost
 module SZ = FStar.SizeT
 open Pulse.Lib.SmallType
+open Pulse.Lib.SendSync
 
 [@@erasable] val base_t : Type0
 
@@ -45,6 +45,8 @@ val is_null #a (r: array a) : b:bool {b <==> r == null #a}
 
 val pts_to_mask (#t: Type u#a) ([@@@mkey] a: array t) (#[full_default()] f: perm) (v: erased (Seq.seq t)) (mask: nat -> prop) : slprop
 
+instance val is_send_pts_to_mask #a r #p n m : is_send (pts_to_mask #a r #p n m)
+
 val pts_to_mask_timeless (#a:Type u#a) (x:array a) (p:perm) (s:Seq.seq a) mask
   : Lemma (timeless (pts_to_mask x #p s mask))
           [SMTPat (timeless (pts_to_mask x #p s mask))]
diff --git a/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fst b/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fst
index 95cc332b6..cb62e732f 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fst
+++ b/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fst
@@ -28,6 +28,8 @@ open Pulse.Lib.WithPure
 let pts_to (#elt: Type u#a) (a: array elt) (#p: perm) (s: Seq.seq elt) : Tot slprop =
   pts_to_mask a #p s fun i -> True
 
+let is_send_pts_to _ _ = Tactics.Typeclasses.solve
+
 ghost fn to_mask u#a (#t: Type u#a) (arr: array t) #f (#v: erased _)
   requires arr |-> Frac f v
   ensures pts_to_mask arr #f v (fun _ -> True)
diff --git a/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fsti b/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fsti
index cc7f74a19..dcc80cd85 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Array.PtsTo.fsti
@@ -26,6 +26,7 @@ module SZ = FStar.SizeT
 module Seq = FStar.Seq
 open Pulse.Lib.Array.Core
 open Pulse.Lib.SmallType
+open Pulse.Lib.SendSync
 
 val pts_to (#a:Type u#a) ([@@@mkey]x:array a) (#[exact (`1.0R)] p:perm) (s: Seq.seq a) : slprop
 
@@ -38,6 +39,8 @@ instance has_pts_to_larray (a:Type u#a) (n : nat) : has_pts_to (larray a n) (Seq
   pts_to = pts_to;
 }
 
+instance val is_send_pts_to #a r #p n : is_send (pts_to #a r #p n)
+
 ghost fn to_mask u#a (#t: Type u#a) (arr: array t) #f (#v: erased _)
   requires arr |-> Frac f v
   ensures pts_to_mask arr #f v (fun _ -> True)
diff --git a/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fst b/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fst
index aeb4914c1..861914151 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fst
+++ b/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fst
@@ -39,6 +39,8 @@ let pts_to_range
 : slprop
 = with_pure (i <= j /\ j <= length x) fun _ -> pts_to (gsub x i j) #p s
 
+let is_send_pts_to_range x i j p s = Tactics.Typeclasses.solve
+
 ghost fn fold_pts_to_range u#a (#a: Type u#a) (x: array a) (i: nat) (j: nat { i <= j /\ j <= length x }) #p #s0 s #mask
   requires pts_to_mask (gsub x i j) #p s0 mask
   requires pure (Seq.equal s s0)
diff --git a/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fsti b/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fsti
index 7b8e962dc..827989568 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Array.PtsToRange.fsti
@@ -24,6 +24,7 @@ open PulseCore.FractionalPermission
 open FStar.Ghost
 module SZ = FStar.SizeT
 module Seq = FStar.Seq
+open Pulse.Lib.SendSync
 open Pulse.Lib.Array.Core
 open Pulse.Lib.Array.PtsTo
 
@@ -35,6 +36,9 @@ val pts_to_range
   (#[exact (`1.0R)] p:perm)
   (s : Seq.seq a) : slprop
 
+instance val is_send_pts_to_range (#a: Type u#a) (x:array a) (i j : nat) (p:perm) (s:Seq.seq a)
+  : is_send (pts_to_range x i j #p s)
+
 val pts_to_range_timeless (#a: Type u#a) (x:array a) (i j : nat) (p:perm) (s:Seq.seq a)
   : Lemma (timeless (pts_to_range x i j #p s))
           [SMTPat (timeless (pts_to_range x i j #p s))]
diff --git a/lib/pulse/lib/Pulse.Lib.Box.fst b/lib/pulse/lib/Pulse.Lib.Box.fst
index 7bb86a223..f0a9f7f45 100644
--- a/lib/pulse/lib/Pulse.Lib.Box.fst
+++ b/lib/pulse/lib/Pulse.Lib.Box.fst
@@ -33,6 +33,8 @@ let is_null #a (r : box a)
 
 let pts_to b #p v = R.pts_to b.r #p v ** pure (R.is_full_ref b.r)
 
+let is_send_pts_to _ _ = Tactics.Typeclasses.solve
+
 let pts_to_timeless _ _ _ = ()
 
 (* This function is extracted primitively. The implementation
diff --git a/lib/pulse/lib/Pulse.Lib.Box.fsti b/lib/pulse/lib/Pulse.Lib.Box.fsti
index cb634d5fe..d64db6a59 100644
--- a/lib/pulse/lib/Pulse.Lib.Box.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Box.fsti
@@ -22,6 +22,7 @@ open PulseCore.FractionalPermission
 
 open Pulse.Lib.Core
 open Pulse.Class.PtsTo
+open Pulse.Lib.SendSync
 
 module T = FStar.Tactics.V2
 module R = Pulse.Lib.Reference
@@ -38,6 +39,8 @@ val pts_to (#a:Type0)
            (#[T.exact (`1.0R)] p:perm)
            (v:a) : slprop
 
+instance val is_send_pts_to #a b #p v : is_send (pts_to #a b #p v)
+
 [@@pulse_unfold]
 instance has_pts_to_box (a:Type u#0) : has_pts_to (box a) a = {
   pts_to = pts_to;
diff --git a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
index e7fe941cb..b11b50e26 100644
--- a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
+++ b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
@@ -32,12 +32,28 @@ instance non_informative_cinv = {
 
 let cinv_vp_aux (r:GR.ref bool) (v:slprop) :slprop =
   exists* (b:bool). pts_to r #0.5R b **
-                    (if b then v else emp)
+                    cond b v emp
+
+irreducible instance placeless_cond c a b {| da: placeless a, db: placeless b |} :
+    placeless (cond c a b) =
+  if c then da else db
+
+irreducible instance is_send_cond c a b {| da: is_send a, db: is_send b |} :
+    is_send (cond c a b) =
+  if c then da else db
 
 let cinv_vp c v = cinv_vp_aux c.r v
 
+instance placeless_cinv_vp_aux c v {| placeless v |} : placeless (cinv_vp c v) =
+  Tactics.Typeclasses.solve
+
+instance is_send_cinv_vp_aux c v {| is_send v |} : is_send (cinv_vp c v) =
+  Tactics.Typeclasses.solve
+
 let active c p = pts_to c.r #(p /. 2.0R) true
 
+let placeless_active c p = Tactics.Typeclasses.solve
+
 let active_timeless p c = ()
 
 let iname_of c = c.i
@@ -51,7 +67,8 @@ fn new_cancellable_invariant (v:slprop)
   ensures inv (iname_of c) (cinv_vp c v) ** active c 1.0R
 {
   let r = GR.alloc true;
-  rewrite v as (if true then v else emp);
+  rewrite v as cond true v emp;
+  // somewhere_intro (cond true v emp) #_;
   GR.share r;
   fold (cinv_vp_aux r v);
   let i = new_invariant (cinv_vp_aux r v);
@@ -62,7 +79,7 @@ fn new_cancellable_invariant (v:slprop)
 }
 
 
-let unpacked c _v = pts_to c.r #0.5R true
+let unpacked c v = pts_to c.r #0.5R true
 
 ghost
 fn unpack_cinv_vp (#p:perm) (#v:slprop) (c:cinv)
@@ -72,10 +89,11 @@ fn unpack_cinv_vp (#p:perm) (#v:slprop) (c:cinv)
 {
   unfold cinv_vp;
   unfold cinv_vp_aux;
-  with b. assert (pts_to c.r #0.5R b ** (if b then v else emp));
+  with b. assert cond b v emp;
+  assert (pts_to c.r #0.5R b ** (cond b v emp));
   unfold active;
   GR.pts_to_injective_eq c.r;
-  rewrite (if b then v else emp) as v;
+  rewrite cond b v emp as v;
   fold (active c p);
   fold (unpacked c v)
 }
@@ -89,7 +107,7 @@ fn pack_cinv_vp (#v:slprop) (c:cinv)
   opens []
 {
   unfold unpacked;
-  rewrite v as (if true then v else emp);
+  rewrite v as cond true v emp;
   fold (cinv_vp_aux c.r v);
   fold (cinv_vp c v)
 }
@@ -132,14 +150,14 @@ fn cancel_ (#v:slprop) (c:cinv)
 {
   unfold cinv_vp;
   unfold cinv_vp_aux;
-  with b. assert (pts_to c.r #0.5R b ** (if b then v else emp));
+  with b. assert (pts_to c.r #0.5R b ** (cond b v emp));
   unfold active;
   GR.pts_to_injective_eq c.r;
-  rewrite (if b then v else emp) as v;
+  rewrite cond b v emp as v;
   GR.gather c.r;
   GR.(c.r := false);
-  rewrite emp as (if false then v else emp);
   GR.share c.r;
+  rewrite emp as (cond false v emp);
   fold (cinv_vp_aux c.r v);
   fold (cinv_vp c v);
   drop_ (pts_to c.r #0.5R _)
@@ -154,13 +172,9 @@ fn cancel (#v:slprop) (c:cinv)
   ensures v
   opens [iname_of c]
 {
-  with_invariants (iname_of c)
-    returns _:unit
-    ensures later (cinv_vp c v) ** v
-    opens [iname_of c] {
-    later_elim _;
+  with_inv_g unit emp_inames (iname_of c) (cinv_vp c v)
+      (active c 1.0R) (fun _ -> v) fn _ {
     cancel_ c;
-    later_intro (cinv_vp c v);
   };
   drop_ (inv (iname_of c) _)
 }
diff --git a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fsti b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fsti
index 3be6a34d6..eddea7264 100644
--- a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fsti
+++ b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fsti
@@ -18,6 +18,7 @@ module Pulse.Lib.CancellableInvariant
 #lang-pulse
 
 open Pulse.Lib.Pervasives
+open Pulse.Lib.SendSync
 
 [@@ erasable]
 val cinv : Type0
@@ -27,8 +28,13 @@ instance val non_informative_cinv
 
 val cinv_vp ([@@@mkey] c:cinv) (v:slprop) : slprop
 
+instance val placeless_cinv_vp_aux c v {| placeless v |} : placeless (cinv_vp c v)
+instance val is_send_cinv_vp_aux c v {| is_send v |} : is_send (cinv_vp c v)
+
 val active ([@@@mkey] c:cinv) (p:perm) : slprop
 
+instance val placeless_active c p : placeless (active c p)
+
 val active_timeless (c:cinv) (p:perm)
   : Lemma (timeless (active c p))
           [SMTPat (timeless (active c p))]
diff --git a/lib/pulse/lib/Pulse.Lib.ConditionVar.fst b/lib/pulse/lib/Pulse.Lib.ConditionVar.fst
index 5108a75e9..d109f73f6 100644
--- a/lib/pulse/lib/Pulse.Lib.ConditionVar.fst
+++ b/lib/pulse/lib/Pulse.Lib.ConditionVar.fst
@@ -17,6 +17,7 @@
 module Pulse.Lib.ConditionVar
 #lang-pulse
 open Pulse.Lib.Pervasives
+open Pulse.Lib.SendableTrade
 module U32 = FStar.UInt32
 module OR = Pulse.Lib.OnRange
 module SLT = Pulse.Lib.SLPropTable
@@ -35,7 +36,6 @@ type cvar_t = {
 }
 
 let singleton #a (i:a) = Seq.create 1 i
-let full_perm : perm = 1.0R
 
 let predicate_at (t:SLT.table) (f:perm) (pred:Seq.seq slprop) (i:nat)
 : slprop
@@ -43,16 +43,66 @@ let predicate_at (t:SLT.table) (f:perm) (pred:Seq.seq slprop) (i:nat)
   then SLT.pts_to t i #f (Seq.index pred i)
   else emp
 
+instance placeless_predicate_at t f pred i : placeless (predicate_at t f pred i) =
+  if i < Seq.length pred then
+    SLT.placeless_pts_to t i #f (Seq.index pred i)
+  else
+    placeless_emp
+
 [@@pulse_unfold]
 let stored_predicates (t:SLT.table) (n:nat) (f:perm) (pred:Seq.seq slprop) 
 = OR.on_range (predicate_at t f pred) 0 n
 
 let index_preds (pred:Seq.seq slprop) (i:nat)
-= if i < Seq.length pred then Seq.index pred i else emp
+= if i < Seq.length pred then sendable (Seq.index pred i) else emp
+
+instance is_send_index_preds pred i : is_send (index_preds pred i) =
+  if i < Seq.length pred then is_send_sendable (Seq.index pred i) else is_send_placeless emp
 
 let istar (pred:Seq.seq slprop) 
 = OR.on_range (index_preds pred) 0 (Seq.length pred)
 
+ghost fn rec is_send_on_range' p (i j: nat) (l: loc_id) {| (k:nat -> is_send (p k)) |}
+  requires in_same_process l
+  requires OR.on_range p i j
+  ensures on l (OR.on_range p i j)
+  decreases j
+{
+  if (i > j) {
+    OR.on_range_eq_false p i j;
+    rewrite OR.on_range p i j as pure False;
+    unreachable ()
+  } else if (i = j) {
+    OR.on_range_empty_elim p i;
+    drop_ (in_same_process l);
+    ghost_impersonate l emp (on l (OR.on_range p i j)) fn _ {
+      OR.on_range_empty p i;
+      on_intro (OR.on_range p i j);
+    }
+  } else {
+    OR.on_range_unsnoc () #p #i #j;
+    is_send_intro_on (p (j-1)) l;
+    is_send_on_range' p i (j-1) l #_;
+    ghost_impersonate l
+        (on l (p (j - 1)) ** on l (OR.on_range p i (j - 1)))
+        (on l (OR.on_range p i j)) fn _ {
+      on_elim (p (j - 1));
+      on_elim _;
+      OR.on_range_snoc ();
+      on_intro (OR.on_range p i j);
+    }
+  }
+}
+
+ghost fn is_send_on_range p i j {| (k:nat -> is_send (p k)) |} : is_send (OR.on_range p i j) = l1 l2 {
+  ghost_impersonate l1 (on l1 (OR.on_range p i j)) (on l2 (OR.on_range p i j)) fn _ {
+    on_elim _;
+    loc_dup l1;
+    fold in_same_process l2;
+    is_send_on_range' p i j l2 #_;
+  }
+}
+
 ghost
 fn weaken_on_range (f g: (nat -> slprop))
                    (i j:nat)
@@ -67,16 +117,13 @@ ensures
   OR.on_range_weaken f g i j fn k { rewrite f k as g k }
 }
 
-let istar_singleton (p:slprop)
-: Lemma (istar (singleton p) == p)
-= slprop_equivs ();
-  OR.on_range_eq_emp (index_preds (singleton p)) 1 1;
-  OR.on_range_eq_cons (index_preds (singleton p)) 0 1
-
 let maybe_holds (v:U32.t) (p:slprop) (pred:Seq.seq slprop)
 : slprop
-= if v = 0ul then equiv (istar pred) p else istar pred
+= if v = 0ul then trade p (istar pred) else istar pred
 
+instance is_send_maybe_holds v p pred : is_send (maybe_holds v p pred) =
+  if v = 0ul then is_send_trade #emp_inames p (istar pred)
+    else is_send_on_range (index_preds pred) 0 (Seq.length pred)
 
 let cvar_inv (b: cvar_t_core) (p:slprop)
 : slprop
@@ -104,7 +151,10 @@ let recv (b: cvar_t) (p:slprop)
     cvar b q **
     SLT.pts_to b.core.tab i #0.5R p
 
-fn create (p:slprop)
+instance is_send_send c p : is_send (send c p) = Tactics.Typeclasses.solve
+instance is_send_recv c p : is_send (recv c p) = Tactics.Typeclasses.solve
+
+fn create (p:slprop) {| is_send p |}
   requires emp
   returns c:cvar_t
   ensures send c p ** recv c p
@@ -117,10 +167,13 @@ fn create (p:slprop)
       as (predicate_at tab 0.5R (singleton p) 0);
   OR.on_range_singleton_intro (predicate_at tab 0.5R (singleton p)) 0;
   Box.share r;
-  istar_singleton p;
-  equiv_refl (istar (singleton p));
-  rewrite (equiv (istar (singleton p)) (istar (singleton p)))
-      as  (maybe_holds 0ul p (singleton p));
+  intro (p @==> istar (singleton p)) fn _ {
+    sendable_intro p #_;
+    rewrite sendable p as index_preds (singleton p) 0;
+    OR.on_range_singleton_intro (index_preds (singleton p)) 0;
+    fold istar (singleton p);
+  };
+  fold maybe_holds 0ul p (singleton p);
   let core = { r; tab };
   rewrite each r as core.r;
   rewrite each tab as core.tab;
@@ -129,7 +182,7 @@ fn create (p:slprop)
   let cv = { core; i };
   rewrite each core as cv.core;
   rewrite each i as cv.i;
-  dup_inv cv.i _;
+  dup (inv cv.i (cvar_inv cv.core p)) ();
   fold (cvar cv p);
   fold (send cv p);
   fold (cvar cv p);
@@ -147,24 +200,18 @@ ensures
 {
   unfold send;
   unfold cvar;
-  with_invariants b.i
-  returns _:unit
-  ensures later (cvar_inv b.core p)
+  with_inv_atomic unit emp_inames b.i (cvar_inv b.core p)
+    (p ** Box.pts_to b.core.r #0.5R 0ul) (fun _ -> emp) fn _
   {
-     later_elim _;
      unfold cvar_inv;
      Box.gather b.core.r;
-     with v preds. assert (maybe_holds v p preds);
-     assert pure (v == 0ul);
+     with v preds. unfold (maybe_holds (reveal v) p preds);
+     assert rewrites_to v 0ul;
      write_atomic_box b.core.r 1ul;
-     rewrite (maybe_holds v p preds)
-        as  (equiv (istar preds) p);
-     equiv_comm _ _;
-     equiv_elim p (istar preds);
-     rewrite (istar preds) as (maybe_holds 1ul p preds);
+     elim_trade p (istar preds);
+     fold (maybe_holds 1ul p preds);
      Box.share b.core.r;
      fold (cvar_inv b.core p);
-     later_intro (cvar_inv b.core p);
      drop_ (Box.pts_to b.core.r #0.5R _)
   };
   drop_ (inv _ _)
@@ -235,21 +282,18 @@ ensures
   with q. assert (cvar b q);
   unfold cvar;
   later_credit_buy 1;
-  later_credit_buy 1;
-  // show_proof_state;
-  let res:bool =
-    with_invariants b.i
-    returns res:bool
-    ensures later (cvar_inv b.core q) **
-            (if res then p else SLT.pts_to b.core.tab i #0.5R p)
+  let res =
+    with_inv_stt bool emp_inames b.i (cvar_inv b.core q)
+      (SLT.pts_to b.core.tab i #0.5R p ** later_credit 1)
+      (fun res -> cond res p (SLT.pts_to b.core.tab i #0.5R p))
+      fn _
     {
-      later_elim _;
       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);
+        fold cond false p (SLT.pts_to b.core.tab i #0.5R p);
         drop_ (later_credit 1);
         false;
       }
@@ -259,14 +303,16 @@ ensures
         rewrite (maybe_holds v q preds)
           as (istar preds);
         get_predicate_at_i b.core.tab i p preds;
-        later_elim _;
         unfold istar;
         OR.on_range_get i #(index_preds preds);
-        rewrite (index_preds preds i) as (Seq.index preds i);
+        rewrite (index_preds preds i) as sendable (Seq.index preds i);
+        sendable_elim (Seq.index preds i);
+        later_elim (equiv _ _);
         equiv_elim _ _;
         SLT.update b.core.tab i emp;
         let preds' : erased (Seq.seq slprop) = FStar.Seq.upd preds i emp;
-        rewrite emp as (index_preds preds' i);
+        sendable_intro emp #_;
+        rewrite sendable emp as (index_preds preds' i);
         weaken_and_put
             (index_preds preds)
             (index_preds preds')
@@ -282,13 +328,14 @@ 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);
         drop_ (SLT.pts_to b.core.tab i #0.5R _);
+        fold cond true p (SLT.pts_to b.core.tab i #0.5R p);
         true
       }
     };
-  if res { drop_ (inv b.i _); () } 
+  if res { drop_ (inv b.i _); elim_cond_true _ _ _; } 
   else { 
+    elim_cond_false _ _ _;
     fold (cvar b q);
     fold (recv b p);
     wait b #p
@@ -296,108 +343,7 @@ ensures
 }
 
 ghost
-fn equiv_star_cong_r (p q r x:slprop)
-requires
-  equiv (p ** x) r **
-  equiv x q
-ensures
-  equiv (p ** q) r
-{
-  equiv_star_congr p x q;
-  rewrite (equiv x q) as (equiv x q ** equiv (p ** x) (p ** q));
-  equiv_comm (p ** x) (p ** q);
-  equiv_trans (p ** q) (p ** x) r;
-  drop_ (equiv x q)
-}
-
-let istar_preds_preds'_eq
-      (preds:Seq.seq slprop) 
-      (i:nat{ i < Seq.length preds })
-      (p1 p2:slprop)
-: Lemma (
-  let preds' = FStar.Seq.(snoc (snoc (Seq.upd preds i emp) p1) p2) in
-  istar preds == 
-  OR.on_range (index_preds preds') 0 (Seq.length preds) ** Seq.index preds i)
-= let preds' = FStar.Seq.(snoc (snoc (Seq.upd preds i emp) p1) p2) in
-  calc (==) {
-    istar preds;
-  (==) {}
-    OR.on_range (index_preds preds) 0 (Seq.length preds);
-  (==) { OR.on_range_eq_get (index_preds preds) 0 i (Seq.length preds) }
-    OR.on_range (index_preds preds) 0 i ** index_preds preds i ** OR.on_range (index_preds preds) (i + 1) (Seq.length preds);
-  (==) { 
-      OR.on_range_frame (index_preds preds) (index_preds preds') 0 i;
-      OR.on_range_frame (index_preds preds) (index_preds preds') (i + 1) (Seq.length preds) 
-      }
-    OR.on_range (index_preds preds') 0 i ** index_preds preds i ** OR.on_range (index_preds preds') (i + 1) (Seq.length preds);
-  (==) { slprop_equivs () }
-    (OR.on_range (index_preds preds') 0 i ** index_preds preds' i ** OR.on_range (index_preds preds') (i + 1) (Seq.length preds)) **
-    index_preds preds i;
-  (==) { OR.on_range_eq_get (index_preds preds') 0 i (Seq.length preds) }
-    OR.on_range (index_preds preds') 0 (Seq.length preds) ** Seq.index preds i;
-  }
-
-let istar_preds'_tail 
-      (preds:Seq.seq slprop) 
-      (i:nat{ i < Seq.length preds })
-      (p1 p2:slprop)
-: Lemma (
-    let preds' = FStar.Seq.(snoc (snoc (Seq.upd preds i emp) p1) p2) in
-    p1 ** p2 == (OR.on_range (index_preds preds') (Seq.length preds) (Seq.length preds')))
-=     let preds' = FStar.Seq.(snoc (snoc (Seq.upd preds i emp) p1) p2) in
-  OR.on_range_eq_emp (index_preds preds') (Seq.length preds') (Seq.length preds');
-  OR.on_range_eq_cons (index_preds preds') (Seq.length preds) (Seq.length preds');
-  OR.on_range_eq_cons (index_preds preds') (Seq.length preds + 1) (Seq.length preds');
-  slprop_equivs ()
-
-ghost
-fn rewrite_istar_equiv (preds:Seq.seq slprop) (preds':Seq.seq slprop) (i:nat{ i < Seq.length preds }) (p1 p2 q:slprop)
-requires
-  pure (preds' == FStar.Seq.(snoc (snoc (Seq.upd preds i emp) p1) p2)) **
-  equiv (istar preds) q **
-  later (equiv (Seq.index preds i) (p1 ** p2)) **
-  later_credit 1
-ensures
-  equiv (istar preds') q
-{
-  later_elim _;
-  istar_preds_preds'_eq preds i p1 p2;
-  rewrite
-    equiv (istar preds) q
-  as
-    equiv (OR.on_range (index_preds preds') 0 (Seq.length preds) ** Seq.index preds i) q
-  ;
-  equiv_star_cong_r _ _ _ _;
-  istar_preds'_tail preds i p1 p2;
-  OR.on_range_join_eq 0 (Seq.length preds) (Seq.length preds') (index_preds preds');
-
-  rewrite equiv (OR.on_range (index_preds preds') 0 (Seq.length preds) ** (p1 ** p2)) q
-       as equiv (istar preds') q;
-}
-
-ghost
-fn rewrite_istar (preds:Seq.seq slprop) (preds':Seq.seq slprop) (i:nat{ i < Seq.length preds }) (p1 p2 q:slprop)
-requires
-  pure (preds' == FStar.Seq.(snoc (snoc (Seq.upd preds i emp) p1) p2)) **
-  istar preds **
-  later (equiv (Seq.index preds i) (p1 ** p2)) **
-  later_credit 1
-ensures
-  istar preds'
-{ 
-  later_elim _;
-  istar_preds_preds'_eq preds i p1 p2;
-  rewrite (istar preds) as (OR.on_range (index_preds preds') 0 (Seq.length preds) ** Seq.index preds i);
-  equiv_elim _ _;
-  istar_preds'_tail preds i p1 p2;
-  rewrite (p1 ** p2)
-  as (OR.on_range (index_preds preds') (Seq.length preds) (Seq.length preds'));
-  OR.on_range_join 0 (Seq.length preds) (Seq.length preds') #(index_preds preds');
-  fold (istar preds')
-}
-
-ghost
-fn split (b:cvar_t) (#p1 #p2:slprop)
+fn split (b:cvar_t) (#p1 #p2:slprop) {| is_send p1, is_send p2 |}
 requires 
   recv b (p1 ** p2) ** later_credit 2
 ensures
@@ -412,16 +358,13 @@ opens
   with i. assert (SLT.pts_to b.core.tab i #0.5R (p1 ** p2));
   with q. assert (cvar b q);
   unfold cvar;
-  let _ : unit =
-    with_invariants b.i
-    returns _:unit
-    ensures
-      later (cvar_inv b.core q) **
+  with_inv_g unit emp_inames b.i (cvar_inv b.core q)
+    (later_credit 1 ** SLT.pts_to b.core.tab i #0.5R (p1 ** p2))
+    (fun _ ->
       (exists* j k.
         SLT.pts_to b.core.tab j #0.5R p1 **
-        SLT.pts_to b.core.tab k #0.5R p2)
-    {
-      later_elim _;
+        SLT.pts_to b.core.tab k #0.5R p2))
+    fn _ {
       unfold cvar_inv;
       with v preds. assert (maybe_holds v q preds);
       get_predicate_at_i b.core.tab i (p1 ** p2) preds;
@@ -445,30 +388,49 @@ opens
       rewrite SLT.pts_to b.core.tab (Seq.length preds + 1) #0.5R p2
           as (predicate_at b.core.tab 0.5R preds' (Seq.length preds + 1));
       OR.on_range_snoc();
+      later_elim (equiv _ _);
+      intro (istar preds @==> istar preds')
+          #(equiv (Seq.Base.index preds i) (p1 ** p2)) fn _ {
+        unfold istar preds;
+        OR.on_range_get i;
+        weaken_on_range (index_preds preds) (index_preds preds') 0 i;
+        weaken_on_range (index_preds preds) (index_preds preds') (i+1) (Seq.length preds);
+        sendable_intro emp #_;
+        rewrite sendable emp as index_preds preds' i;
+        OR.on_range_put 0 i (Seq.length preds);
+        rewrite index_preds preds i as sendable (Seq.index preds i);
+        sendable_elim (Seq.index preds i);
+        equiv_elim _ _;
+        sendable_intro p1 #_; rewrite sendable p1 as index_preds preds' (Seq.length preds);
+        sendable_intro p2 #_; rewrite sendable p2 as index_preds preds' (Seq.length preds + 1);
+        OR.on_range_snoc ();
+        OR.on_range_snoc ();
+        fold istar preds';
+      };
       let vz = (reveal v = 0ul);
       if (vz)
       {
-        rewrite (maybe_holds v q preds) as (equiv (istar preds) q);
+        rewrite (maybe_holds v q preds) as (q @==> istar preds);
         OR.on_range_eq_get (index_preds preds) 0 i (Seq.length preds);
-        rewrite_istar_equiv preds preds' i p1 p2 q;
-        // show_proof_state;
-        // step ();
-        rewrite equiv (istar preds') q as maybe_holds v q preds';
+        intro (q @==> istar preds')
+            #(trade q (istar preds) ** trade (istar preds) (istar preds')) fn _ {
+          elim_trade q (istar preds);
+          elim_trade (istar preds) (istar preds');
+        };
+        rewrite (q @==> istar preds') as (maybe_holds v q preds');
         fold (cvar_inv b.core q);
-        later_intro (cvar_inv b.core q);
         drop_ (SLT.pts_to b.core.tab i #0.5R emp);
       }
       else
       { 
         rewrite (maybe_holds v q preds) as (istar preds);
-        rewrite_istar preds preds' i p1 p2 q;
-        rewrite istar preds' as maybe_holds v q preds';
+        elim_trade (istar preds) (istar preds');
+        rewrite (istar preds') as (maybe_holds v q preds');
         fold (cvar_inv b.core q);
-        later_intro (cvar_inv b.core q);
         drop_ (SLT.pts_to b.core.tab i #0.5R emp);
       }
     };
-  dup_inv b.i _;
+  dup (inv b.i (cvar_inv b.core q)) ();
   fold (cvar b q);
   fold (recv b p1);
   fold (cvar b q);
diff --git a/lib/pulse/lib/Pulse.Lib.ConditionVar.fsti b/lib/pulse/lib/Pulse.Lib.ConditionVar.fsti
index 9b6661102..c7ad20de1 100644
--- a/lib/pulse/lib/Pulse.Lib.ConditionVar.fsti
+++ b/lib/pulse/lib/Pulse.Lib.ConditionVar.fsti
@@ -17,6 +17,8 @@
 module Pulse.Lib.ConditionVar
 #lang-pulse
 open Pulse.Lib.Pervasives
+open Pulse.Lib.SendSync
+
 val cvar_t : Type0
 
 val inv_name (c:cvar_t) : iname
@@ -25,7 +27,10 @@ val send (c:cvar_t) (p:slprop) : slprop
 
 val recv (c:cvar_t) (p:slprop) : slprop
 
-fn create (p:slprop)
+instance val is_send_send c p : is_send (send c p)
+instance val is_send_recv c p : is_send (recv c p)
+
+fn create (p:slprop) {| is_send p |}
   requires emp
   returns c:cvar_t
   ensures send c p ** recv c p
@@ -45,7 +50,7 @@ fn wait (b:cvar_t) (#p:slprop)
   ensures p
 
 ghost
-fn split (b:cvar_t) (#p #q:slprop)
+fn split (b:cvar_t) (#p #q:slprop) {| is_send p, is_send q |}
   requires recv b (p ** q) ** later_credit 2
   ensures recv b p ** recv b q
   opens [ inv_name b ]
diff --git a/lib/pulse/lib/Pulse.Lib.FlippableInv.fst b/lib/pulse/lib/Pulse.Lib.FlippableInv.fst
index 69eef3210..062ab1d07 100644
--- a/lib/pulse/lib/Pulse.Lib.FlippableInv.fst
+++ b/lib/pulse/lib/Pulse.Lib.FlippableInv.fst
@@ -43,7 +43,7 @@ let on  #p (fi : finv p) : slprop =
   pts_to fi.r #0.5R true ** inv fi.i (finv_p p fi.r)
 
 
-fn mk_finv (p:slprop)
+ghost fn mk_finv (p:slprop)
    requires emp
    returns f:(finv p)
    ensures off f
@@ -68,7 +68,7 @@ fn mk_finv (p:slprop)
 let iname_of #p (f : finv p) : iname = f.i
 
 
-atomic
+ghost
 fn flip_on (#p:slprop) (fi:finv p)
    requires off fi ** p ** later_credit 1
    ensures on fi
@@ -76,27 +76,22 @@ fn flip_on (#p:slprop) (fi:finv p)
 {
   open Pulse.Lib.GhostReference;
   unfold off;
-  with_invariants fi.i
-    returns _:unit
-    ensures later (finv_p p fi.r) **
-            pts_to fi.r #0.5R true
-    opens [fi.i]
+  with_inv_g unit emp_inames fi.i (finv_p p fi.r)
+    (p ** pts_to fi.r #0.5R false) (fun _ -> pts_to fi.r #0.5R true) fn _
   {
-    later_elim _;
     unfold finv_p;
     with b.
       assert (pts_to fi.r #0.5R b ** pts_to fi.r #0.5R false);
-    GR.gather fi.r;
+    GR.gather fi.r #false #_;
     rewrite each b as false;
     fi.r := true;
     GR.share fi.r;
     fold_finv_p p fi.r;
-    later_intro (finv_p p fi.r);
   };
   fold on fi;
 }
 
-atomic
+ghost
 fn flip_off (#p:slprop) (fi : finv p)
    requires on fi ** later_credit 1
    ensures off fi ** p
@@ -104,13 +99,9 @@ fn flip_off (#p:slprop) (fi : finv p)
 {
   open Pulse.Lib.GhostReference;
   unfold on;
-  with_invariants fi.i
-    returns _:unit
-    ensures later (finv_p p fi.r) **
-            pts_to fi.r #0.5R false ** p
-    opens [fi.i]
+  with_inv_g unit emp_inames fi.i (finv_p p fi.r)
+    (pts_to fi.r #0.5R true) (fun _ -> p ** pts_to fi.r #0.5R false) fn _
   {
-    later_elim _;
     unfold finv_p;
     with b.
       assert (pts_to fi.r #0.5R b ** pts_to fi.r #0.5R true);
@@ -119,7 +110,6 @@ fn flip_off (#p:slprop) (fi : finv p)
     fi.r := false;
     GR.share fi.r;
     fold_finv_p p fi.r;
-    later_intro (finv_p p fi.r);
   };
   fold off fi;
 }
diff --git a/lib/pulse/lib/Pulse.Lib.FlippableInv.fsti b/lib/pulse/lib/Pulse.Lib.FlippableInv.fsti
index b59719c4a..649a164e0 100644
--- a/lib/pulse/lib/Pulse.Lib.FlippableInv.fsti
+++ b/lib/pulse/lib/Pulse.Lib.FlippableInv.fsti
@@ -24,12 +24,15 @@ val finv (p:slprop) : Type0
 val off #p (fi : finv p) : slprop
 val on  #p (fi : finv p) : slprop
 
-val mk_finv (p:slprop) : stt (finv p) emp (fun x -> off x)
+ghost
+fn mk_finv (p:slprop)
+  returns x:finv p
+  ensures off x
 
 val iname_of #p (f : finv p) : iname
 
 
-atomic
+ghost
 fn flip_on (#p:slprop) (fi : finv p)
   requires off fi ** p ** later_credit 1
   ensures on fi
@@ -37,7 +40,7 @@ fn flip_on (#p:slprop) (fi : finv p)
 
 
 
-atomic
+ghost
 fn flip_off (#p:slprop) (fi : finv p)
   requires on fi ** later_credit 1
   ensures  off fi ** p
diff --git a/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fst b/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fst
index 159178a6a..2c8223150 100644
--- a/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fst
+++ b/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fst
@@ -35,11 +35,15 @@ let is_table #a ([@@@mkey]t:table a) (max:nat)
 : slprop
 = GPR.pts_to t (full_table_above max)
 
+let placeless_is_table #a t max = Tactics.Typeclasses.solve
+
 let pts_to #a (t:table a) (i:nat) (#f:perm) (p:a)
 : slprop
 = GPR.pts_to t (singleton i f (Some p)) **
   pure (PF.perm_ok f)
 
+let placeless_pts_to #a t i #f p = Tactics.Typeclasses.solve
+
 ghost
 fn create (#a:Type)
   requires emp
diff --git a/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fsti b/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fsti
index db2186029..9493ab172 100644
--- a/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fsti
+++ b/lib/pulse/lib/Pulse.Lib.GhostFractionalTable.fsti
@@ -8,8 +8,12 @@ val table (a:Type0) : Type0
 instance val non_informative_table (a:Type): NonInformative.non_informative (table a)
 val is_table #a ([@@@mkey] t:table a) (max:nat) : slprop
 
+instance val placeless_is_table #a t max : placeless (is_table #a t max)
+
 val pts_to #a ([@@@mkey] t:table a) (i:nat) (#f:perm) (p:a) : slprop
 
+instance val placeless_pts_to #a t i #f p : placeless (pts_to #a t i #f p)
+
 ghost
 fn create (#a:Type)
   requires emp
diff --git a/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fst b/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fst
index 8d97fcbdf..206fb87a0 100644
--- a/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fst
+++ b/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fst
@@ -32,6 +32,10 @@ let small_token (inst: small_type u#a) = emp
 let pts_to (#a:Type u#a) (#p:pcm a) ([@@@mkey] r:ghost_pcm_ref p) (v:a) : slprop =
   exists* (inst: small_type u#a). C.ghost_pcm_pts_to #_ #(raise p) r (U.raise_val v) ** small_token inst
 
+instance pts_to_placeless #a #p r v =
+  placeless_exists _ #(fun inst ->
+    placeless_star _ _ #(C.placeless_ghost_pcm_pts_to #_ #(raise p) r (U.raise_val v)) #_)
+
 let pts_to_is_timeless #a #p r v =
   assert_norm (pts_to r v ==
     op_exists_Star fun (inst: small_type u#a) ->
diff --git a/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fsti b/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fsti
index b6a16f9ea..a79f2940e 100644
--- a/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fsti
+++ b/lib/pulse/lib/Pulse.Lib.GhostPCMReference.fsti
@@ -47,6 +47,13 @@ val pts_to
     (v:a)
 : slprop
 
+instance val pts_to_placeless
+    (#a:Type)
+    (#p:pcm a)
+    (r:gref p)
+    (v:a)
+: placeless (pts_to r v)
+
 val pts_to_is_timeless
     (#a:Type)
     (#p:pcm a)
diff --git a/lib/pulse/lib/Pulse.Lib.GhostReference.fst b/lib/pulse/lib/Pulse.Lib.GhostReference.fst
index 9864ebf12..fd785d0fe 100644
--- a/lib/pulse/lib/Pulse.Lib.GhostReference.fst
+++ b/lib/pulse/lib/Pulse.Lib.GhostReference.fst
@@ -29,6 +29,7 @@ let null #a = GR.null_core_ghost_pcm_ref
 let pts_to (#a:Type) (r:ref a) (#[T.exact (`1.0R)] p:perm) (n:a)
 = GR.pts_to r (Some (n, p)) ** pure (perm_ok p)
 
+let pts_to_placeless r p n = Tactics.Typeclasses.solve
 let pts_to_timeless _ _ _ = ()
 
 
diff --git a/lib/pulse/lib/Pulse.Lib.GhostReference.fsti b/lib/pulse/lib/Pulse.Lib.GhostReference.fsti
index d1f633f45..762cb59af 100644
--- a/lib/pulse/lib/Pulse.Lib.GhostReference.fsti
+++ b/lib/pulse/lib/Pulse.Lib.GhostReference.fsti
@@ -46,6 +46,9 @@ instance has_pts_to_ref (a:Type u#a) : has_pts_to (ref a) a = {
   pts_to = (fun r #f v -> pts_to r #f v);
 }
 
+instance val pts_to_placeless (#a:Type u#a) (r:ref a) (p:perm) (n:a) :
+  placeless (pts_to r #p n)
+
 val pts_to_timeless (#a:Type u#a) (r:ref a) (p:perm) (n:a)
   : Lemma (timeless (pts_to r #p n)) [SMTPat (timeless (pts_to r #p n))]
 
diff --git a/lib/pulse/lib/Pulse.Lib.Inv.fst b/lib/pulse/lib/Pulse.Lib.Inv.fst
new file mode 100644
index 000000000..a5874e4e4
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.Inv.fst
@@ -0,0 +1,197 @@
+module Pulse.Lib.Inv
+#lang-pulse
+open Pulse.Lib.Core
+open Pulse.Lib.SendSync
+open Pulse.Class.Duplicable
+module C = Pulse.Lib.Core.Inv
+
+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 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. _;
+    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
+      {
+        bwd ();
+        let f = f; f ()
+      };
+      ghost fn g' ()
+        requires on l' p
+        ensures on l2 p
+      {
+        let g = g; g ();
+        fwd ();
+      };
+      fold move_tag l2 l' p f' g';
+      loc_dup l2;
+      fold inv i p;
+      on_intro (inv i p);
+    }
+  }
+}
+
+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. _;
+  C.dup_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 }
+
+ghost fn fresh_invariant
+    (ctx: inames { Pulse.Lib.GhostSet.is_finite ctx })
+    (p: slprop)
+  requires p
+  returns i: iname
+  ensures inv i p
+  ensures pure (~(Pulse.Lib.GhostSet.mem i ctx))
+{
+  loc_get (); with l. assert loc l;
+  on_intro p;
+  let i = C.fresh_invariant ctx (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
+}
+
+ghost fn new_invariant (p: slprop)
+  requires p
+  returns i: iname
+  ensures inv i p
+{
+  fresh_invariant emp_inames p
+}
+
+inline_for_extraction noextract
+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 ** 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 = C.with_invariant #a #Neutral
+      #(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
+}
+
+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
+{
+  ghost fn k ()
+    opens is
+    requires pre ** p
+    returns x: Ghost.erased a
+    ensures post x ** p
+  {
+    let r = k ();
+    r
+  };
+  let r = with_inv_unobs (Ghost.erased a) is i p pre (fun r -> post r) fn _ { k () };
+  r
+}
+
+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. _;
+  let x = C.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_intro p;
+    { let f=f; f() };
+    later_intro (on l' p);
+    x
+  };
+  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
+}
\ No newline at end of file
diff --git a/lib/pulse/lib/Pulse.Lib.Inv.fsti b/lib/pulse/lib/Pulse.Lib.Inv.fsti
new file mode 100644
index 000000000..13eb426a1
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.Inv.fsti
@@ -0,0 +1,79 @@
+module Pulse.Lib.Inv
+#lang-pulse
+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 dup_inv (i:iname) (p:slprop)
+  preserves inv i p
+  ensures inv i p
+{
+  dup (inv i p) ()
+}
+
+ghost fn fresh_invariant
+    (ctx: inames { Pulse.Lib.GhostSet.is_finite ctx })
+    (p: slprop)
+  requires p
+  returns i: iname
+  ensures inv i p
+  ensures pure (~(Pulse.Lib.GhostSet.mem i ctx))
+
+ghost fn new_invariant (p: slprop)
+  requires p
+  returns i: iname
+  ensures inv i p
+
+inline_for_extraction noextract
+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 ** 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
+
+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
\ No newline at end of file
diff --git a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
index 67257e136..830f7b877 100644
--- a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
+++ b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
@@ -25,6 +25,7 @@ let pts_to' (#t:Type)
     pure (f <=. 1.0R /\ Cons? h /\ PulseCore.Preorder.curval h == v)
 
 let pts_to = pts_to'
+let placeless_pts_to r v = Tactics.Typeclasses.solve
 let pts_to_is_timeless (#t:Type) (#p:preorder t) (r:mref p) #f (v:t) = ()
 
 [@@pulse_unfold]
diff --git a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti
index b978d1a4a..beb679de2 100644
--- a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti
+++ b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti
@@ -20,6 +20,9 @@ val pts_to (#t:Type)
            (v:t)
 : slprop
 
+instance val placeless_pts_to (#t:Type) (#p:preorder t) (r:mref p) (#f:perm) (v:t)
+: placeless (pts_to r #f v)
+
 val pts_to_is_timeless (#t:Type) (#p:preorder t) (r:mref p) (#f:perm) (v:t)
 : Lemma (timeless (pts_to r #f v))
         [SMTPat (timeless (pts_to r #f v))]
diff --git a/lib/pulse/lib/Pulse.Lib.Mutex.fst b/lib/pulse/lib/Pulse.Lib.Mutex.fst
index 6c2e25b8d..8c8c91cd8 100644
--- a/lib/pulse/lib/Pulse.Lib.Mutex.fst
+++ b/lib/pulse/lib/Pulse.Lib.Mutex.fst
@@ -40,6 +40,8 @@ let lock_inv (#a:Type0) (r:B.box a) (v:a -> slprop) : slprop =
 
 let mutex_live #a m #p v = lock_alive m.l #p (lock_inv m.r v)
 
+let is_send_mutex_live #a m #p v #_ = Tactics.Typeclasses.solve
+
 let pts_to mg #p x = pts_to mg #p x
 
 let op_Bang #a mg #x #p = R.op_Bang #a mg #x #p
diff --git a/lib/pulse/lib/Pulse.Lib.Mutex.fsti b/lib/pulse/lib/Pulse.Lib.Mutex.fsti
index 2600d3d6f..46d976a63 100644
--- a/lib/pulse/lib/Pulse.Lib.Mutex.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Mutex.fsti
@@ -18,6 +18,7 @@ module Pulse.Lib.Mutex
 #lang-pulse
 
 open Pulse.Lib.Pervasives
+open Pulse.Lib.SendSync
 
 module T = FStar.Tactics.V2
 
@@ -35,6 +36,8 @@ val mutex_live
   (#[T.exact (`1.0R)] p:perm)
   (v:a -> slprop)  : slprop
 
+instance val is_send_mutex_live #a m #p v {| (x:a -> is_send (v x)) |} : is_send (mutex_live #a m #p v)
+
 //
 // mutex_guard is a ref-like type
 //
diff --git a/lib/pulse/lib/Pulse.Lib.OnRange.fst b/lib/pulse/lib/Pulse.Lib.OnRange.fst
index 40327b29a..e01aec08c 100644
--- a/lib/pulse/lib/Pulse.Lib.OnRange.fst
+++ b/lib/pulse/lib/Pulse.Lib.OnRange.fst
@@ -494,3 +494,44 @@ fn rec on_range_unzip (p q:nat -> slprop) (i j:nat)
   }
 }
 
+ghost fn rec on_range_move p (i j: nat) (l1 l2: loc_id)
+    (f: (k:nat -> stt_ghost unit emp_inames (on l1 (p k)) (fun _ -> on l2 (p k))))
+  requires on l1 (on_range p i j)
+  ensures on l2 (on_range p i j)
+  decreases j
+{
+  ghost_impersonate l1 (on l1 (on_range p i j)) (on l2 (on_range p i j)) fn _ {
+    on_elim _;
+    if (i > j) {
+      on_range_eq_false p i j;
+      rewrite on_range p i j as pure False;
+      unreachable ()
+    } else if (i = j) {
+      on_range_empty_elim p i;
+      ghost_impersonate l2 emp (on l2 (on_range p i j)) fn _ {
+        on_range_empty p i;
+        on_intro (on_range p i j);
+      }
+    } else {
+      on_range_unsnoc () #p #i #j;
+      on_intro (p (j-1)); f (j-1);
+      on_intro (on_range p i (j-1)); on_range_move p i (j-1) l1 l2 f;
+      ghost_impersonate l2
+          (on l2 (p (j - 1)) ** on l2 (on_range p i (j - 1)))
+          (on l2 (on_range p i j)) fn _ {
+        on_elim (p (j - 1));
+        on_elim (on_range p i (j - 1));
+        on_range_snoc ();
+        on_intro (on_range p i j);
+      }
+    }
+  }
+}
+
+ghost fn placeless_on_range p i j {| inst : (k:nat -> placeless (p k)) |} : placeless (on_range p i j) = l1 l2 {
+  on_range_move p i j l1 l2 fn k { inst k l1 l2 }
+}
+
+ghost fn is_send_on_range p i j {| (k:nat -> is_send (p k)) |} : is_send (on_range p i j) = l1 l2 {
+  on_range_move p i j l1 l2 fn k { is_send_elim (p k) l2 }
+}
diff --git a/lib/pulse/lib/Pulse.Lib.OnRange.fsti b/lib/pulse/lib/Pulse.Lib.OnRange.fsti
index f005fd2d8..5ad47e9d5 100644
--- a/lib/pulse/lib/Pulse.Lib.OnRange.fsti
+++ b/lib/pulse/lib/Pulse.Lib.OnRange.fsti
@@ -18,6 +18,7 @@ module Pulse.Lib.OnRange
 #lang-pulse
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Trade
+open Pulse.Lib.SendSync
 
 val on_range ([@@@mkey] p: (nat -> slprop))
              (i:nat)
@@ -231,3 +232,6 @@ val on_range_unzip (p q:nat -> slprop) (i j:nat)
   : stt_ghost unit emp_inames
       (on_range (fun k -> p k ** q k) i j)
       (fun _ -> on_range p i j ** on_range q i j)
+
+instance val placeless_on_range p i j {| (k:nat -> placeless (p k)) |} : placeless (on_range p i j)
+instance val is_send_on_range p i j {| (k:nat -> is_send (p k)) |} : is_send (on_range p i j)
diff --git a/lib/pulse/lib/Pulse.Lib.PCMReference.fst b/lib/pulse/lib/Pulse.Lib.PCMReference.fst
index a8955a43c..1ea6f78e8 100644
--- a/lib/pulse/lib/Pulse.Lib.PCMReference.fst
+++ b/lib/pulse/lib/Pulse.Lib.PCMReference.fst
@@ -39,6 +39,9 @@ let timeless_pcm_pts_to #a #p r v =
     op_exists_Star fun (inst: small_type u#a) ->
       C.pcm_pts_to #_ #(raise p) r (U.raise_val v) ** small_token inst)
 
+let placeless_pcm_pts_to #a #p r v =
+  Tactics.Typeclasses.solve
+
 ghost fn pts_to_small u#a (#a:Type u#a) (#p:FStar.PCM.pcm a) (r:pcm_ref p) (v:a)
   preserves pcm_pts_to r v
   returns inst: small_type u#a
diff --git a/lib/pulse/lib/Pulse.Lib.PCMReference.fsti b/lib/pulse/lib/Pulse.Lib.PCMReference.fsti
index 65e56ebe7..44cadcd39 100644
--- a/lib/pulse/lib/Pulse.Lib.PCMReference.fsti
+++ b/lib/pulse/lib/Pulse.Lib.PCMReference.fsti
@@ -38,6 +38,8 @@ val pcm_pts_to (#a:Type u#a) (#p:pcm a) ([@@@mkey] r:pcm_ref p) (v:a) : slprop
 val timeless_pcm_pts_to (#a:Type u#a) (#p:pcm a) (r:pcm_ref p) (v:a)
 : Lemma (timeless (pcm_pts_to r v)) [SMTPat (timeless (pcm_pts_to r v))]
 
+instance val placeless_pcm_pts_to #a #p r v : placeless (pcm_pts_to #a #p r v)
+
 ghost fn pts_to_small u#a (#a: Type u#a) (#p:FStar.PCM.pcm a) (r:pcm_ref p) (v:a)
   preserves pcm_pts_to r v
   returns inst: small_type u#a
diff --git a/lib/pulse/lib/Pulse.Lib.Par.fst b/lib/pulse/lib/Pulse.Lib.Par.fst
index 1d96d5f65..54f1e0b89 100644
--- a/lib/pulse/lib/Pulse.Lib.Par.fst
+++ b/lib/pulse/lib/Pulse.Lib.Par.fst
@@ -19,14 +19,15 @@ open Pulse.Lib.ConditionVar
 
 #lang-pulse
 
-fn par_stt' #preL #postL #preR #postR
+fn par_stt' (#preL: slprop) #postL #preR #postR
+  {| is_send preL, is_send postL |}
   (f:unit -> stt unit preL (fun _ -> postL))
   (g:unit -> stt unit preR (fun _ -> postR))
   requires preL ** preR
   ensures postL ** postR
 {
-  let c = create postL;
-  fork #(preL ** send c postL) fn _ {
+  let c = create postL #_;
+  fork' (preL ** send c postL) fn _ {
     f ();
     signal c #postL;
   };
diff --git a/lib/pulse/lib/Pulse.Lib.Par.fsti b/lib/pulse/lib/Pulse.Lib.Par.fsti
index 06447ea3e..cd379c770 100644
--- a/lib/pulse/lib/Pulse.Lib.Par.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Par.fsti
@@ -16,12 +16,14 @@
 module Pulse.Lib.Par
 #lang-pulse
 open Pulse.Lib.Core
+open Pulse.Lib.SendSync
 
 val par_stt
   (#preL:slprop)
   (#postL:slprop)
   (#preR:slprop)
   (#postR:slprop)
+  {| is_send preL, is_send postL |}
   (f:stt unit preL (fun _ -> postL))
   (g:stt unit preR (fun _ -> postR))
 : stt unit
diff --git a/lib/pulse/lib/Pulse.Lib.Pervasives.fst b/lib/pulse/lib/Pulse.Lib.Pervasives.fst
index ad451fb59..0ee9b9bad 100644
--- a/lib/pulse/lib/Pulse.Lib.Pervasives.fst
+++ b/lib/pulse/lib/Pulse.Lib.Pervasives.fst
@@ -18,6 +18,8 @@ module Pulse.Lib.Pervasives
 #lang-pulse
 include Pulse.Main
 include Pulse.Lib.Core
+include Pulse.Lib.Inv
+include Pulse.Lib.SendSync
 include Pulse.Lib.Forall
 include Pulse.Lib.Array
 include Pulse.Lib.Reference
diff --git a/lib/pulse/lib/Pulse.Lib.Reference.fst b/lib/pulse/lib/Pulse.Lib.Reference.fst
index 9c727f145..960b06c67 100644
--- a/lib/pulse/lib/Pulse.Lib.Reference.fst
+++ b/lib/pulse/lib/Pulse.Lib.Reference.fst
@@ -36,6 +36,8 @@ let upd_singleton #a (x y: a) :
 
 let pts_to (#a: Type u#a) (r:ref a) (#[T.exact (`1.0R)] p:perm) (n:a)
 = A.pts_to r #p (singleton n)
+let is_send_pts_to r n = Tactics.Typeclasses.solve
+
 let pts_to_timeless _ _ _ = ()
 
 let is_full_ref = A.is_full_array
diff --git a/lib/pulse/lib/Pulse.Lib.Reference.fsti b/lib/pulse/lib/Pulse.Lib.Reference.fsti
index 35757d8be..f51494f8f 100644
--- a/lib/pulse/lib/Pulse.Lib.Reference.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Reference.fsti
@@ -23,6 +23,7 @@ open FStar.Ghost
 open Pulse.Class.PtsTo
 open Pulse.Lib.Array.Basic
 open Pulse.Lib.SmallType
+open Pulse.Lib.SendSync
 module T = FStar.Tactics
 val ref ([@@@unused]a:Type) : Type0
 
@@ -32,6 +33,8 @@ val is_null #a (r : ref a) : b:bool{b <==> r == null #a}
 
 val pts_to (#a:Type u#a) ([@@@mkey]r:ref a) (#[T.exact (`1.0R)] p:perm) (n:a) : slprop
 
+instance val is_send_pts_to #a r #p n : is_send (pts_to #a r #p n)
+
 [@@pulse_unfold]
 instance has_pts_to_ref (a:Type u#a) : has_pts_to (ref a) a = {
   pts_to = (fun r #f v -> pts_to r #f v);
diff --git a/lib/pulse/lib/Pulse.Lib.SLPropTable.fst b/lib/pulse/lib/Pulse.Lib.SLPropTable.fst
index b11ecf664..bda0b6ad4 100644
--- a/lib/pulse/lib/Pulse.Lib.SLPropTable.fst
+++ b/lib/pulse/lib/Pulse.Lib.SLPropTable.fst
@@ -13,12 +13,16 @@ let is_table (t:table) (max:nat)
 : slprop
 = GT.is_table t max
 
+let placeless_is_table t max = Tactics.Typeclasses.solve
+
 let pts_to ([@@@mkey]t:table) ([@@@mkey]i:nat) (#f:perm) (p:slprop)
 : slprop
 = exists* r.
     slprop_ref_pts_to r p **
     GT.pts_to t i #f r
 
+let placeless_pts_to t i #f p = Tactics.Typeclasses.solve
+
 ghost
 fn create ()
   requires emp
diff --git a/lib/pulse/lib/Pulse.Lib.SLPropTable.fsti b/lib/pulse/lib/Pulse.Lib.SLPropTable.fsti
index 340b4f600..e19dee0ce 100644
--- a/lib/pulse/lib/Pulse.Lib.SLPropTable.fsti
+++ b/lib/pulse/lib/Pulse.Lib.SLPropTable.fsti
@@ -9,8 +9,12 @@ instance val non_informative_table: NonInformative.non_informative table
 
 val is_table ([@@@mkey]t:table) (max:nat) : slprop
 
+instance val placeless_is_table t max : placeless (is_table t max)
+
 val pts_to ([@@@mkey]t:table) ([@@@mkey]i:nat) (#f:perm) (p:slprop) : slprop
 
+instance val placeless_pts_to t i #f p : placeless (pts_to t i #f p)
+
 ghost
 fn create ()
   requires emp
diff --git a/lib/pulse/lib/Pulse.Lib.SendSync.fst b/lib/pulse/lib/Pulse.Lib.SendSync.fst
new file mode 100644
index 000000000..38104bd0f
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.SendSync.fst
@@ -0,0 +1,246 @@
+module Pulse.Lib.SendSync
+open Pulse.Lib.Core
+open Pulse.Class.Duplicable
+open Pulse.Main
+#lang-pulse
+
+let timeless_in_same_process p =
+  assert_norm (in_same_process p == (exists* l. loc l ** pure (process_of l == process_of p)))
+
+ghost fn dup_in_same_process p () : duplicable_f (in_same_process p) = {
+  unfold in_same_process p;
+  loc_dup _;
+  fold in_same_process p;
+  fold in_same_process p;
+}
+
+instance duplicable_in_same_process p : duplicable (in_same_process p) =
+  { dup_f = dup_in_same_process p }
+
+ghost fn on_star_elim #l (p q: slprop)
+  requires on l (p ** q)
+  ensures on l p
+  ensures on l q
+{
+  ghost_impersonate l (on l (p ** q)) (on l p ** on l q) fn _ {
+    on_elim (p ** q);
+    on_intro p;
+    on_intro q;
+  }
+}
+
+ghost fn on_star_intro #l (p q: slprop)
+  requires on l p
+  requires on l q
+  ensures on l (p ** q)
+{
+  ghost_impersonate l (on l p ** on l q) (on l (p ** q)) fn _ {
+    on_elim p;
+    on_elim q;
+    on_intro (p ** q);
+  }
+}
+
+ghost fn on_exists_elim u#a #l (#a: Type u#a) (p: a -> slprop)
+  requires on l (exists* x. p x)
+  ensures exists* x. on l (p x)
+{
+  ghost_impersonate l (on l (exists* x. p x)) (exists* x. on l (p x)) fn _ {
+    on_elim (exists* x. p x);
+    on_intro (p _);
+  }
+}
+
+ghost fn is_send_elim p {| inst: is_send p |} #l l'
+  requires on l p
+  requires pure (process_of l == process_of l')
+  ensures on l' p
+{
+  inst l l'
+}
+
+ghost fn is_send_elim_on p {| is_send p |} #l
+  preserves in_same_process l
+  requires on l p
+  ensures p
+{
+  unfold in_same_process l;
+  with l0. assert loc l0;
+  is_send_elim p l0;
+  on_elim p;
+  fold in_same_process l;
+}
+
+ghost fn is_send_intro_on p {| is_send p |} l
+  preserves in_same_process l
+  requires p
+  ensures on l p
+{
+  unfold in_same_process l;
+  with l0. assert loc l0;
+  on_intro p;
+  is_send_elim p l;
+  fold in_same_process l;
+}
+
+ghost fn is_send_elim_on' p {| is_send p |} #l
+  preserves loc l
+  requires on (process_of l) p
+  ensures p
+{
+  loc_dup l;
+  fold in_same_process (process_of l);
+  is_send_elim_on p #_;
+  drop_ (in_same_process (process_of l));
+}
+
+ghost fn is_send_intro_on' p {| is_send p |} l
+  preserves loc l
+  requires p
+  ensures on (process_of l) p
+{
+  loc_dup l;
+  fold in_same_process (process_of l);
+  is_send_intro_on p (process_of l);
+  drop_ (in_same_process (process_of l));
+}
+
+ghost fn is_send_placeless p {| inst: placeless p |} : is_send p = l l' {
+  inst l l'
+}
+
+ghost fn is_send_in_same_process p : is_send (in_same_process p) = l l' {
+  ghost_impersonate l
+    (on l (in_same_process p))
+    (on l' (in_same_process p))
+    fn _ {
+      on_elim (in_same_process p);
+      unfold in_same_process p;
+      loc_gather l #_;
+      ghost_impersonate l' emp (on l' (in_same_process p)) fn _ {
+        loc_dup l';
+        fold in_same_process p;
+        on_intro (in_same_process p);
+      }
+    }
+}
+
+ghost fn is_send_star p q {| is_send p, is_send q |} : is_send (p ** q) = l l' {
+  on_star_elim p q;
+  is_send_elim p l';
+  is_send_elim q l';
+  on_star_intro p q;
+}
+
+ghost fn is_send_exists' u#a (#a: Type u#a) (p: a->slprop) {| ((x:a) -> is_send (p x)) |} :
+    is_send (exists* x. p x) = l l' {
+  ghost_impersonate l (on l (exists* x. p x)) (on l' (exists* x. p x)) fn _ {
+    on_elim (exists* x. p x);
+    with x. assert p x;
+    on_intro (p x);
+    is_send_elim (p x) l';
+    ghost_impersonate l' (on l' (p x)) (on l' (exists* x. p x)) fn _ {
+      on_elim (p x);
+      on_intro (exists* x. p x)
+    };
+  }
+}
+let is_send_exists = is_send_exists'
+
+let on_same_process (p: slprop) =
+  exists* l. in_same_process l ** on l p
+
+ghost fn on_same_process_elim p {| is_send p |}
+  requires on_same_process p
+  ensures p
+{
+  unfold on_same_process p;
+  is_send_elim_on p #_;
+  drop_ (in_same_process _);
+}
+
+ghost fn on_same_process_intro p
+  requires p
+  ensures on_same_process p
+{
+  loc_get (); with l. assert loc l;
+  on_intro p;
+  fold in_same_process l;
+  fold on_same_process p;
+}
+
+let timeless_on_same_process p =
+  assert_norm (on_same_process p == (exists* l. in_same_process l ** on l p))
+
+ghost fn is_send_on_same_process p : is_send (on_same_process p) = l1 l2 {
+  ghost_impersonate l1
+    (on l1 (on_same_process p))
+    (on l2 (on_same_process p))
+    fn _ {
+      on_elim (on_same_process p);
+      unfold on_same_process p; with l. _;
+      unfold in_same_process l; with l1'. _;
+      loc_gather l1 #l1';
+      ghost_impersonate l2
+        (on l p)
+        (on l2 (on_same_process p))
+        fn _ {
+          loc_dup l2; fold in_same_process l;
+          fold on_same_process p;
+          on_intro (on_same_process p);
+        }
+    }
+}
+
+let is_send_tag ([@@@mkey] p: slprop) (inst: is_send p) = emp
+let sendable p = exists* inst. is_send_tag p inst ** p
+
+ghost fn sendable_elim p
+  requires sendable p
+  ensures p
+{
+  unfold sendable p;
+  drop_ (is_send_tag p _);
+}
+
+ghost fn sendable_intro p {| inst: is_send p |}
+  requires p
+  ensures sendable p
+{
+  fold is_send_tag p inst;
+  fold sendable p;
+}
+
+ghost fn is_send_sendable p : is_send (sendable p) = l1 l2 {
+  ghost_impersonate l1 (on l1 (sendable p)) (on l2 (sendable p)) fn _ {
+    on_elim (sendable p);
+    unfold sendable p;
+    with inst. unfold is_send_tag p inst;
+    let inst = inst;
+    on_intro p;
+    is_send_elim p l2;
+    ghost_impersonate l2 (on l2 p) (on l2 (sendable p)) fn _ {
+      on_elim p;
+      fold is_send_tag p inst;
+      fold sendable p;
+      on_intro (sendable p)
+    }
+  }
+}
+
+inline_for_extraction noextract fn fork'
+  (pre:slprop) {| is_send pre |}
+  (f: (unit -> stt unit pre (fun _ -> emp)))
+  requires pre
+{
+  loc_get (); with l. assert loc l;
+  loc_dup l; fold in_same_process (process_of l);
+  is_send_intro_on pre (process_of l);
+  drop_ (in_same_process (process_of l));
+  fork (on (process_of l) pre) #_ #l fn l' {
+    fold in_same_process (process_of l);
+    is_send_elim_on pre #_;
+    drop_ (in_same_process (process_of l));
+    f ();
+  };
+}
\ No newline at end of file
diff --git a/lib/pulse/lib/Pulse.Lib.SendSync.fsti b/lib/pulse/lib/Pulse.Lib.SendSync.fsti
new file mode 100644
index 000000000..0927f89b4
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.SendSync.fsti
@@ -0,0 +1,70 @@
+module Pulse.Lib.SendSync
+open Pulse.Lib.Core
+open Pulse.Class.Duplicable
+open Pulse.Main
+#lang-pulse
+
+let in_same_process p = exists* l. loc l ** pure (process_of l == process_of p)
+val timeless_in_same_process p : Lemma (timeless (in_same_process p)) [SMTPat (timeless (in_same_process p))]
+instance val duplicable_in_same_process p : duplicable (in_same_process p)
+
+[@@Tactics.Typeclasses.tcclass; erasable]
+type is_send (p: slprop) =
+  l:loc_id -> l':loc_id { process_of l == process_of l' } ->
+    stt_ghost unit emp_inames (on l p) (fun _ -> on l' p)
+
+ghost fn is_send_elim p {| inst: is_send p |} #l l'
+  requires on l p
+  requires pure (process_of l == process_of l')
+  ensures on l' p
+
+ghost fn is_send_elim_on p {| is_send p |} #l
+  preserves in_same_process l
+  requires on l p
+  ensures p
+
+ghost fn is_send_intro_on p {| is_send p |} l
+  preserves in_same_process l
+  requires p
+  ensures on l p
+
+ghost fn is_send_elim_on' p {| is_send p |} #l
+  preserves loc l
+  requires on (process_of l) p
+  ensures p
+
+ghost fn is_send_intro_on' p {| is_send p |} l
+  preserves loc l
+  requires p
+  ensures on (process_of l) p
+
+instance val is_send_placeless p {| inst: placeless p |} : is_send p
+instance val is_send_in_same_process p : is_send (in_same_process p)
+instance val is_send_star p q {| is_send p, is_send q |} : is_send (p ** q)
+instance val is_send_exists #a (p: a->slprop) {| ((x:a) -> is_send (p x)) |} :
+  is_send (exists* x. p x)
+
+val on_same_process (p: slprop) : slprop
+ghost fn on_same_process_elim p {| is_send p |}
+  requires on_same_process p
+  ensures p
+ghost fn on_same_process_intro p
+  requires p
+  ensures on_same_process p
+val timeless_on_same_process (p: timeless_slprop) :
+  Lemma (timeless (on_same_process p)) [SMTPat (timeless (on_same_process p))]
+instance val is_send_on_same_process p : is_send (on_same_process p)
+
+val sendable (p: slprop) : slprop
+ghost fn sendable_elim p
+  requires sendable p
+  ensures p
+ghost fn sendable_intro p {| is_send p |}
+  requires p
+  ensures sendable p
+instance val is_send_sendable p : is_send (sendable p)
+
+inline_for_extraction noextract fn fork'
+  (pre:slprop) {| is_send pre |}
+  (f: (unit -> stt unit pre (fun _ -> emp)))
+  requires pre
\ No newline at end of file
diff --git a/lib/pulse/lib/Pulse.Lib.SpinLock.fst b/lib/pulse/lib/Pulse.Lib.SpinLock.fst
index 96578ae15..a3785b6fc 100644
--- a/lib/pulse/lib/Pulse.Lib.SpinLock.fst
+++ b/lib/pulse/lib/Pulse.Lib.SpinLock.fst
@@ -32,6 +32,12 @@ let lock_inv_aux (r:B.box U32.t) (gr:GR.ref U32.t) (v:slprop) : slprop  =
                pure ((i == 0ul ==> p == 1.0R) /\
                      (i =!= 0ul ==> p == 0.5R)) 
 
+instance 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
+
+instance is_send_lock_inv_aux r gr v {| is_send v |} : is_send (lock_inv_aux r gr v) =
+  Tactics.Typeclasses.solve
+
 let lock_inv (r:B.box U32.t) (gr:GR.ref U32.t) (v:slprop) : slprop =
   lock_inv_aux r gr v
 
@@ -43,9 +49,13 @@ type lock = {
   i : cinv;
 }
 
+let is_send_tag v (inst: is_send v) = emp
+
 let lock_alive l #p v =
   inv (iname_of l.i) (cinv_vp l.i (lock_inv l.r l.gr v)) ** active l.i p
 
+instance is_send_lock_alive = Tactics.Typeclasses.solve
+
 let lock_acquired l = pts_to l.gr #0.5R 1ul
 
 
@@ -54,9 +64,9 @@ fn new_lock (v:slprop)
   returns l:lock
   ensures lock_alive l v
 {
-  let r = B.alloc 0ul;
   let gr = GR.alloc 0ul;
   rewrite v as (if 0ul = 0ul then v else emp);
+  let r = B.alloc 0ul;
   fold (lock_inv_aux r gr v);
   fold (lock_inv r gr v);
   let i = new_cancellable_invariant (lock_inv r gr v);
@@ -68,21 +78,18 @@ fn new_lock (v:slprop)
   l
 }
 
-
-
 fn rec acquire (#v:slprop) (#p:perm) (l:lock)
   preserves lock_alive l #p v
   ensures v ** lock_acquired l
 {
   unfold (lock_alive l #p v);
-  later_credit_buy 1;
   let b =
-    with_invariants (CInv.iname_of l.i)
-      returns b:bool
-      ensures later (cinv_vp l.i (lock_inv l.r l.gr v)) **
-              active l.i p **
-              (if b then v ** pts_to l.gr #0.5R 1ul else emp) {
-      later_elim _;
+    with_inv_stt bool emp_inames (CInv.iname_of l.i) (cinv_vp l.i (lock_inv l.r l.gr v))
+        (active l.i p)
+        (fun b ->
+          active l.i p **
+          (cond b (v ** pts_to l.gr #0.5R 1ul) emp))
+        fn _ {
       unpack_cinv_vp l.i;
       unfold lock_inv;
       unfold lock_inv_aux;
@@ -102,8 +109,7 @@ fn rec acquire (#v:slprop) (#p:perm) (l:lock)
                 v);
         let b = true;
         rewrite (v ** pts_to l.gr #0.5R 1ul)
-             as (if b then v ** pts_to l.gr #0.5R 1ul else emp);
-        later_intro (CInv.cinv_vp l.i (lock_inv l.r l.gr v));
+             as (cond b (v ** pts_to l.gr #0.5R 1ul) emp);
         b
       } else {
         elim_cond_false _ _ _;
@@ -114,16 +120,17 @@ fn rec acquire (#v:slprop) (#p:perm) (l:lock)
                 active l.i p);
         let b = false;
         rewrite emp as
-                (if b then v ** pts_to l.gr #0.5R 1ul else emp);
-        later_intro (CInv.cinv_vp l.i (lock_inv l.r l.gr v));
+                (cond b (v ** pts_to l.gr #0.5R 1ul) emp);
         b
       }
     };
 
   if b {
+    elim_cond_true b _ _;
     fold (lock_alive l #p v);
     fold (lock_acquired l)
   } else {
+    elim_cond_false b _ _;
     fold (lock_alive l #p v);
     acquire l
   }
@@ -136,27 +143,24 @@ fn release (#v:slprop) (#p:perm) (l:lock)
   requires lock_acquired l ** v
 {
   unfold (lock_alive l #p v);
-  unfold (lock_acquired l);
 
-  later_credit_buy 1;
-  with_invariants (CInv.iname_of l.i)
-    returns _:unit
-    ensures later (cinv_vp l.i (lock_inv l.r l.gr v)) **
-            active l.i p {
-    later_elim _;
+  with_inv_stt unit emp_inames (CInv.iname_of l.i) (cinv_vp l.i (lock_inv l.r l.gr v))
+    (lock_acquired l ** v ** active l.i p)
+    (fun _ -> active l.i p)
+  fn _ {
+    unfold (lock_acquired l);
     unpack_cinv_vp l.i;
     unfold (lock_inv l.r l.gr v);
     unfold (lock_inv_aux l.r l.gr v);
     GR.pts_to_injective_eq l.gr;
     GR.gather l.gr #_ #1ul;
     with i. assert (pts_to l.gr i);
-    rewrite (if (i = 0ul) then v else emp) as emp;
-    write_atomic_box l.r 0ul;
+    rewrite each i as 1ul;
     GR.(l.gr := 0ul);
+    write_atomic_box l.r 0ul;
     fold (lock_inv_aux l.r l.gr v);
     fold (lock_inv l.r l.gr v);
     pack_cinv_vp l.i;
-    later_intro (cinv_vp l.i (lock_inv l.r l.gr v));
   };
 
   fold (lock_alive l #p v)
@@ -184,10 +188,10 @@ fn gather (#v:slprop) (#p1 #p2 :perm) (l:lock)
   ensures lock_alive l #(p1 +. p2) v
 {
   unfold (lock_alive l #p1 v);
+  drop_ (inv (iname_of l.i) _);
   unfold (lock_alive l #p2 v);
   CInv.gather #p1 #p2 l.i;
   fold (lock_alive l #(p1 +. p2) v);
-  drop_ (inv _ _)
 } 
 
 
@@ -200,11 +204,12 @@ fn free (#v:slprop) (l:lock)
   later_credit_buy 1;
   cancel l.i;
   unfold (lock_inv l.r l.gr v);
-  unfold (lock_inv_aux l.r l.gr v);
+  unfold (lock_inv_aux l.r l.gr v); with i. _;
   B.free l.r;
   GR.gather l.gr #_ #1ul;
   with v. assert l.gr |-> v; rewrite each v as 1ul; // awkward
   GR.free l.gr;
+  ()
 }
 
 
@@ -215,76 +220,12 @@ fn lock_alive_inj
   requires lock_alive l #p1 v1 ** lock_alive l #p2 v2
   ensures  lock_alive l #p1 v1 ** lock_alive l #p2 v1
 {
-  unfold (lock_alive l #p1 v1);
   unfold (lock_alive l #p2 v2);
+  drop_ (inv _ _);
+  unfold (lock_alive l #p1 v1);
   dup_inv (CInv.iname_of l.i) (CInv.cinv_vp l.i (lock_inv l.r l.gr v1));
   fold (lock_alive l #p1 v1);
   fold (lock_alive l #p2 v1);
-  drop_ (inv _ _);
   // TODO: we could also prove from, but that requires a significant amount of congruence lemmas about equiv
   // invariant_name_identifies_invariant (CInv.iname_of l.i) (CInv.iname_of l.i);
 }
-
-
-let iname_of l = CInv.iname_of l.i
-let iname_v_of l v = cinv_vp l.i (lock_inv l.r l.gr v)
-let lock_active #p l = active l.i p
-
-
-ghost
-fn share_lock_active (#p:perm) (l:lock)
-  requires lock_active #p l
-  ensures lock_active #(p /. 2.0R) l ** lock_active #(p /. 2.0R) l
-{
-  unfold (lock_active #p l);
-  CInv.share l.i;
-  fold (lock_active #(p /. 2.0R) l);
-  fold (lock_active #(p /. 2.0R) l)
-}
-
-
-
-ghost
-fn gather_lock_active (#p1 #p2:perm) (l:lock)
-  requires lock_active #p1 l ** lock_active #p2 l
-  ensures lock_active #(p1 +. p2) l
-{
-  unfold (lock_active #p1 l);
-  unfold (lock_active #p2 l);
-  CInv.gather #p1 #p2 l.i;
-  fold (lock_active #(p1 +. p2) l)
-}
-
-
-
-ghost
-fn elim_inv_and_active_into_alive (l:lock) (v:slprop) (#p:perm)
-  ensures (inv (iname_of l) (iname_v_of l v) ** lock_active #p l) @==> lock_alive l #p v
-{
-  intro (inv (iname_of l) (iname_v_of l v) ** lock_active #p l @==> lock_alive l #p v) fn _
-  {
-    rewrite each
-      iname_of l as CInv.iname_of l.i,
-      iname_v_of l v as cinv_vp l.i (lock_inv l.r l.gr v);
-    unfold (lock_active #p l);
-    fold (lock_alive l #p v)
-  };
-}
-
-
-
-ghost
-fn elim_alive_into_inv_and_active (l:lock) (v:slprop) (#p:perm)
-  requires emp
-  ensures lock_alive l #p v @==> (inv (iname_of l) (iname_v_of l v) ** lock_active #p l)
-{
-  intro (lock_alive l #p v @==> inv (iname_of l) (iname_v_of l v) ** lock_active #p l) fn _
-  {
-    unfold (lock_alive l #p v);
-    fold (lock_active #p l);
-    rewrite each
-      CInv.iname_of l.i as iname_of l,
-      cinv_vp l.i (lock_inv l.r l.gr v) as iname_v_of l v
-  };
-}
-
diff --git a/lib/pulse/lib/Pulse.Lib.SpinLock.fsti b/lib/pulse/lib/Pulse.Lib.SpinLock.fsti
index 75ba1ca7f..a26b20a78 100644
--- a/lib/pulse/lib/Pulse.Lib.SpinLock.fsti
+++ b/lib/pulse/lib/Pulse.Lib.SpinLock.fsti
@@ -18,6 +18,7 @@ module Pulse.Lib.SpinLock
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Trade
+open Pulse.Lib.SendSync
 
 module T = FStar.Tactics.V2
 
@@ -29,6 +30,8 @@ val lock_alive
       (v:slprop)
   : slprop
 
+instance val is_send_lock_alive l p v {| is_send v |} : is_send (lock_alive l #p v)
+
 val lock_acquired (l:lock) : slprop
 
 fn new_lock (v:slprop)
@@ -66,26 +69,3 @@ fn lock_alive_inj
   (l:lock) (#p1 #p2 :perm) (#v1 #v2 :slprop)
   requires lock_alive l #p1 v1 ** lock_alive l #p2 v2
   ensures  lock_alive l #p1 v1 ** lock_alive l #p2 v1
-
-val iname_of (l:lock) : iname
-val iname_v_of (l:lock) (v:slprop) : slprop
-val lock_active (#[T.exact (`1.0R)] p:perm) (l:lock) : v:slprop { timeless v }
-
-ghost
-fn share_lock_active (#p:perm) (l:lock)
-  requires lock_active #p l
-  ensures lock_active #(p /. 2.0R) l ** lock_active #(p /. 2.0R) l
-
-ghost
-fn gather_lock_active (#p1 #p2:perm) (l:lock)
-  requires lock_active #p1 l ** lock_active #p2 l
-  ensures lock_active #(p1 +. p2) l
-
-ghost
-fn elim_inv_and_active_into_alive (l:lock) (v:slprop) (#p:perm)
-  ensures (inv (iname_of l) (iname_v_of l v) ** lock_active #p l) @==> lock_alive l #p v
-
-ghost
-fn elim_alive_into_inv_and_active (l:lock) (v:slprop) (#p:perm)
-  requires emp
-  ensures lock_alive l #p v @==> (inv (iname_of l) (iname_v_of l v) ** lock_active #p l)
diff --git a/lib/pulse/lib/Pulse.Lib.Task.fst b/lib/pulse/lib/Pulse.Lib.Task.fst
index 2f142ecca..17d5218f1 100644
--- a/lib/pulse/lib/Pulse.Lib.Task.fst
+++ b/lib/pulse/lib/Pulse.Lib.Task.fst
@@ -23,7 +23,6 @@ open FStar.Tactics
 open FStar.Preorder
 open Pulse.Lib.Pledge
 open Pulse.Lib.Trade
-open Pulse.Lib.Shift
 open Pulse.Class.Duplicable
 open Pulse.Class.Introducable
 
@@ -82,14 +81,24 @@ let state_res
   | Done -> post
   | Claimed -> AR.anchored g_state Claimed
 
+instance is_send_state_res pre post g_state st {| is_send pre, is_send post |} :
+    is_send (state_res pre post g_state st) =
+  match st with
+  | Ready -> Tactics.Typeclasses.solve #(is_send pre)
+  | Running -> Tactics.Typeclasses.solve #(is_send emp)
+  | Done -> Tactics.Typeclasses.solve #(is_send post)
+  | Claimed -> Tactics.Typeclasses.solve #(is_send (AR.anchored g_state Claimed))
+
 noeq
 type handle : Type0 = {
   state   : box task_state;
   g_state : AR.ref task_state p_st anchor_rel; (* these two refs are kept in sync *)
 }
 
+let is_send_tag v (inst: is_send v) = emp
+
 let up (x: slprop_ref) : slprop =
-  exists* v. slprop_ref_pts_to x v ** v
+  exists* v inst. slprop_ref_pts_to x v ** is_send_tag v inst ** v
 
 noeq
 type task_t : Type0 = {
@@ -119,25 +128,27 @@ let state_pred
 let task_type (pre post : slprop) : Type0 =
   unit -> task_f pre post
 
-let task_thunk_typing_core (t : task_t) (pre post: slprop) : slprop =
+let task_thunk_typing_core (t : task_t) (pre post: slprop) inst : slprop =
   slprop_ref_pts_to t.pre pre **
   slprop_ref_pts_to t.post post **
+  is_send_tag post inst **
   pure (Dyn.dyn_has_ty t.thunk (task_type pre post))
 
 let task_thunk_typing (t : task_t) : slprop =
-  exists* pre post. task_thunk_typing_core t pre post
+  exists* pre post inst. task_thunk_typing_core t pre post inst
 
 ghost fn task_thunk_typing_dup t
   requires task_thunk_typing t
   ensures task_thunk_typing t ** task_thunk_typing t
 {
   unfold task_thunk_typing t;
-  with pre post. assert task_thunk_typing_core t pre post;
+  with pre post inst. assert task_thunk_typing_core t pre post inst;
   unfold task_thunk_typing_core t pre post;
   slprop_ref_share t.pre;
   slprop_ref_share t.post;
-  fold task_thunk_typing_core t pre post;
-  fold task_thunk_typing_core t pre post;
+  fold is_send_tag post inst;
+  fold task_thunk_typing_core t pre post inst;
+  fold task_thunk_typing_core t pre post inst;
   fold task_thunk_typing t;
   fold task_thunk_typing t;
 }
@@ -155,6 +166,16 @@ let rec all_state_pred
     state_pred t.pre t.post t.h **
     all_state_pred ts
 
+instance is_send_all_state_pred v_runnable : is_send (all_state_pred v_runnable) =
+  let rec is_send_all_state_pred v_runnable : is_send (all_state_pred v_runnable) =
+    match v_runnable with
+    | [] -> is_send_placeless emp
+    | t::ts ->
+      let _: is_send (all_state_pred ts) = is_send_all_state_pred ts in
+      is_send_star (task_thunk_typing t) (state_pred t.pre t.post t.h ** all_state_pred ts) #_
+        #(is_send_star _ _ #_ #_) in
+  is_send_all_state_pred v_runnable
+
 ghost
 fn add_one_state_pred
   (t : task_t)
@@ -232,6 +253,8 @@ type pool : Type0 = pool_st
 let pool_alive (#[exact (`1.0R)] f : perm) (p:pool) : slprop =
   lock_alive p.lk #(f /. 2.0R) (lock_inv p.runnable p.g_runnable)
 
+let is_send_pool_alive p = Tactics.Typeclasses.solve
+
 let state_res' (post : slprop) ( st : task_state) =
   match st with
   | Done -> post
@@ -246,6 +269,65 @@ let task_spotted
     AR.snapshot p.g_runnable v_runnable **
     pure (List.memP t v_runnable)
 
+let shift_tag p q extra (inst1: placeless extra) (inst2: duplicable extra)
+    (f: unit -> stt_ghost unit emp_inames (extra ** p) (fun _ -> q)) =
+  emp
+let shift p q = exists* extra inst1 inst2 f. shift_tag p q extra inst1 inst2 f ** extra
+
+fn introducable_shift_aux u#a (t: Type u#a) is
+    hyp extra concl {| inst1 : placeless extra |} {| inst2: duplicable extra |} {| introducable emp_inames (extra ** hyp) concl t |} (k: t) :
+    stt_ghost unit is extra (fun _ -> shift hyp concl) = {
+  ghost fn f () norewrite requires extra ** hyp ensures concl {
+    intro concl #(extra ** hyp) (fun _ -> k);
+  };
+  fold shift_tag hyp concl extra inst1 inst2 f;
+  fold shift hyp concl;
+}
+
+instance introducable_shift (t: Type u#a) is
+    hyp extra concl {| placeless extra, duplicable extra |} {| introducable emp_inames (extra ** hyp) concl t |} :
+    introducable is extra (shift hyp concl) t =
+  { intro_aux = introducable_shift_aux t is hyp extra concl }
+
+ghost fn dup_shift p q () : duplicable_f (shift p q) = {
+  unfold shift p q;
+  with e i1 i2 f. assert shift_tag p q e i1 i2 f;
+  fold shift_tag p q e i1 i2 f;
+  let i2=i2; dup e ();
+  fold shift p q;
+  fold shift p q;
+}
+instance duplicable_shift p q : duplicable (shift p q) =
+  { dup_f = dup_shift p q }
+
+ghost fn elim_shift p q
+  requires p
+  requires shift p q
+  ensures q
+{
+  unfold shift p q;
+  with e i1 i2 f. assert shift_tag p q e i1 i2 f;
+  unfold shift_tag p q e i1 i2 f;
+  let f = f;
+  f ()
+}
+
+ghost fn placeless_shift' p q : placeless (shift p q) = l1 l2 {
+  ghost_impersonate l1 (on l1 (shift p q)) (on l2 (shift p q)) fn _ {
+    on_elim (shift p q);
+    unfold shift p q;
+    with e i1 i2 f. assert shift_tag p q e i1 i2 f;
+    on_intro e;
+    { let i1=i1; i1 l1 l2; };
+    ghost_impersonate l2 (on l2 e ** shift_tag p q e i1 i2 f) (on l2 (shift p q)) fn _ {
+      on_elim e;
+      fold shift p q;
+      on_intro (shift p q);
+    };
+  }
+}
+instance placeless_shift p q : placeless (shift p q) = placeless_shift' p q
+
 let handle_spotted
   (p : pool)
   (post : slprop)
@@ -256,6 +338,9 @@ let handle_spotted
       shift (up t.post ** later_credit 1) post **
       pure (t.h == h)
 
+instance is_send_handle_spotted p post h : is_send (handle_spotted p post h) =
+  Tactics.Typeclasses.solve
+
 ghost
 fn intro_task_spotted
     (p : pool)
@@ -414,11 +499,12 @@ ghost fn shift_up (x: slprop_ref) (y: slprop)
   ensures shift (up x ** later_credit 1) y
 {
   intro (shift (up x ** later_credit 1) y) #(slprop_ref_pts_to x y) fn _ {
-    unfold up x;
+    unfold up x; with v inst. _;
     slprop_ref_gather _ #_ #y;
     later_elim _;
     equiv_elim _ _;
     drop_ (slprop_ref_pts_to _ _);
+    drop_ (is_send_tag v inst);
   };
 }
 
@@ -430,6 +516,7 @@ fn spawn (p:pool)
     (#pf:perm)
     (#pre : slprop)
     (#post : slprop)
+    {| pre_inst: is_send pre, post_inst: is_send post |}
     (f : unit -> task_f pre post)
     requires pool_alive #pf p ** pre
     returns  h : handle
@@ -458,6 +545,7 @@ fn spawn (p:pool)
   rewrite each post_ref as task.post;
   dup (slprop_ref_pts_to task.pre pre) ();
   dup (slprop_ref_pts_to task.post post) ();
+  fold is_send_tag post post_inst;
   fold task_thunk_typing_core task pre post;
   fold task_thunk_typing task;
   
@@ -490,6 +578,7 @@ fn spawn (p:pool)
   assert (pts_to r_task_st Ready);
 
   rewrite each r_task_st as handle.state;
+  fold is_send_tag pre pre_inst;
   fold up task.pre;
   rewrite (up task.pre)
        as (state_res (up task.pre) (up task.post) gr_task_st Ready);
@@ -806,6 +895,7 @@ fn spawn_ (p:pool)
     (#pf:perm)
     (#pre : slprop)
     (#post : slprop)
+    {| is_send pre, is_send post |}
     (f : unit -> stt unit (pre) (fun _ -> post))
     requires pool_alive #pf p ** pre
     ensures  pool_alive #pf p ** pledge [] (pool_done p) (post)
@@ -1079,9 +1169,9 @@ fn perf_work (t : task_t)
   ensures  up t.post
 {
   unfold task_thunk_typing t;
-  with pre post. assert task_thunk_typing_core t pre post;
+  with pre post inst. assert task_thunk_typing_core t pre post inst;
   unfold task_thunk_typing_core;
-  unfold up;
+  unfold up t.pre;
   slprop_ref_gather t.pre #_ #pre;
   later_credit_buy 1; later_elim _;
   equiv_elim _ _;
@@ -1089,7 +1179,8 @@ fn perf_work (t : task_t)
   undyn pre post t.thunk;
 
   fold up t.post; // ????
-  drop_ (slprop_ref_pts_to _ _);
+  with v vinst. assert is_send_tag v vinst;
+  drop_ (slprop_ref_pts_to _ _ ** is_send_tag v _);
 }
 fn put_back_result (p:pool) #f (t : task_t)
   requires pool_alive #f p **
@@ -1404,7 +1495,7 @@ fn spawn_worker
   requires pool_alive #f p
   ensures  emp
 {
-  fork (fun () -> worker_thread #f p)
+  fork' (pool_alive #f p) (fun () -> worker_thread #f p)
 }
 
 fn rec spawn_workers
diff --git a/lib/pulse/lib/Pulse.Lib.Task.fsti b/lib/pulse/lib/Pulse.Lib.Task.fsti
index f930e0f38..6e3d5217f 100644
--- a/lib/pulse/lib/Pulse.Lib.Task.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Task.fsti
@@ -19,6 +19,7 @@ module Pulse.Lib.Task
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Pledge
+open Pulse.Lib.SendSync
 module T = FStar.Tactics.V2
 
 inline_for_extraction
@@ -27,6 +28,7 @@ let task_f pre post = stt unit pre (fun _ -> post)
 val handle : Type0
 val pool : Type0
 val pool_alive (#[T.exact (`1.0R)] f : perm) (p:pool) : slprop
+instance val is_send_pool_alive #f p : is_send (pool_alive #f p)
 
 val joinable (p: pool) (post: slprop) (h: handle) : slprop
 
@@ -35,6 +37,7 @@ fn spawn
   (#pf: perm)
   (#pre: slprop)
   (#post: slprop)
+  {| is_send pre, is_send post |}
   (f : unit -> task_f pre post)
   requires pool_alive #pf p ** pre
   returns h : handle
@@ -56,6 +59,7 @@ fn spawn_
   (#pf : perm)
   (#pre : slprop)
   (#post : slprop)
+  {| is_send pre, is_send post |}
   (f : unit -> task_f pre post)
   requires pool_alive #pf p ** pre
   ensures pool_alive #pf p ** pledge [] (pool_done p) post
diff --git a/lib/pulse/lib/Pulse.Lib.WithPure.fst b/lib/pulse/lib/Pulse.Lib.WithPure.fst
index 4dd7fb306..f68023608 100644
--- a/lib/pulse/lib/Pulse.Lib.WithPure.fst
+++ b/lib/pulse/lib/Pulse.Lib.WithPure.fst
@@ -8,7 +8,7 @@ let with_pure
   (p : prop)
   (v : squash p -> slprop)
 : slprop
-= op_exists_Star v
+= exists* h. v h
 // Alternative definition:
 // = exists* v'. tag v' ** pure (p /\ v' == v ())
 // much easier to work with, but proving the size wasn't obvious.
@@ -19,56 +19,10 @@ let with_pure_timeless
 : Lemma (requires forall s. timeless (v s))
         (ensures  timeless (with_pure p v))
         [SMTPat (timeless (with_pure p v))]
-= ()
-
-let eta_exists_aux 
-  (#a : Type0)
-  (p : a -> slprop)
-: slprop_equiv (op_exists_Star p) (op_exists_Star (fun (x:a) -> p x))
-= let aux (x:a) : Lemma (slprop_equiv (p x) (p x)) =
-    Squash.return_squash (slprop_equiv_refl (p x))
-  in
-  Classical.forall_intro aux;
-  slprop_equiv_exists p (fun x -> p x) ()
-
-let uneta_exists_aux 
-  (#a : Type0)
-  (p : a -> slprop)
-: slprop_equiv (op_exists_Star (fun (x:a) -> p x)) (op_exists_Star p)
-= let aux (x:a) : Lemma (slprop_equiv (p x) (p x)) =
-    Squash.return_squash (slprop_equiv_refl (p x))
-  in
-  Classical.forall_intro aux;
-  slprop_equiv_exists (fun x -> p x) p ()
-
-
-ghost
-fn eta_exists
-  (a : Type0)
-  (p : a -> slprop)
-  requires op_exists_Star p
-  ensures  op_exists_Star (fun (x:a) -> p x)
-{
-  rewrite op_exists_Star p
-       as op_exists_Star (fun (x:a) -> p x)
-       by apply (`eta_exists_aux);
-}
-
-
-
-ghost
-fn uneta_exists
-  (a : Type0)
-  (p : a -> slprop)
-  requires op_exists_Star (fun (x:a) -> p x)
-  ensures  op_exists_Star p
-{
-  rewrite op_exists_Star (fun (x:a) -> p x)
-       as op_exists_Star p
-       by apply (`uneta_exists_aux);
-}
-
+= assert_norm (with_pure p v == (exists* h. v h))
 
+let placeless_with_pure p v #_ = Tactics.Typeclasses.solve
+let is_send_with_pure p v #_ = Tactics.Typeclasses.solve
 
 ghost
 fn intro_with_pure
@@ -79,8 +33,6 @@ fn intro_with_pure
   ensures  with_pure p v
 {
   assert (v ());
-  assert (exists* s. v s);
-  uneta_exists _ v;
   fold (with_pure p v);
 }
 
@@ -109,7 +61,6 @@ fn elim_with_pure
   ensures  v ()
 {
   unfold (with_pure p v);
-  eta_exists _ v;
   with s. assert (v s);
   squash_single_coerce p v s;
   ()
diff --git a/lib/pulse/lib/Pulse.Lib.WithPure.fsti b/lib/pulse/lib/Pulse.Lib.WithPure.fsti
index a8577c0db..8cd83be4d 100644
--- a/lib/pulse/lib/Pulse.Lib.WithPure.fsti
+++ b/lib/pulse/lib/Pulse.Lib.WithPure.fsti
@@ -1,6 +1,7 @@
 module Pulse.Lib.WithPure
 #lang-pulse
 open Pulse.Lib.Core
+open Pulse.Lib.SendSync
 open Pulse.Main
 
 val with_pure
@@ -14,6 +15,10 @@ val with_pure_timeless
 : Lemma (requires forall s. timeless (v s))
         (ensures  timeless (with_pure p v))
         [SMTPat (timeless (with_pure p v))]
+
+instance val placeless_with_pure (p:prop) v {| (x:squash p -> placeless (v x)) |} : placeless (with_pure p v)
+instance val is_send_with_pure (p:prop) v {| (x:squash p -> is_send (v x)) |} : is_send (with_pure p v)
+
 ghost
 fn intro_with_pure
   (p : prop)
diff --git a/lib/pulse/lib/class/Pulse.Class.Duplicable.fst b/lib/pulse/lib/class/Pulse.Class.Duplicable.fst
index 473c7d53f..6422e906c 100644
--- a/lib/pulse/lib/class/Pulse.Class.Duplicable.fst
+++ b/lib/pulse/lib/class/Pulse.Class.Duplicable.fst
@@ -18,8 +18,3 @@ module Pulse.Class.Duplicable
 #lang-pulse
 
 open Pulse.Lib.Core
-
-instance duplicable_inv (i : iname) (p : slprop)
-  : duplicable (inv i p) = {
-  dup_f = (fun () -> dup_inv i p);
-}
diff --git a/lib/pulse/lib/class/Pulse.Class.Duplicable.fsti b/lib/pulse/lib/class/Pulse.Class.Duplicable.fsti
index 164372eec..2079f1687 100644
--- a/lib/pulse/lib/class/Pulse.Class.Duplicable.fsti
+++ b/lib/pulse/lib/class/Pulse.Class.Duplicable.fsti
@@ -30,5 +30,3 @@ class duplicable (p : slprop) = {
 
 let dup (p : slprop) {| d : duplicable p |} ()
   : stt_ghost unit emp_inames p (fun _ -> p ** p) = d.dup_f ()
-
-instance val duplicable_inv (i : iname) (p : slprop) : duplicable (inv i p)
diff --git a/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fst b/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fst
index 00d854aa8..72e24cd51 100644
--- a/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fst
+++ b/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fst
@@ -18,21 +18,23 @@ module Pulse.Lib.Pledge
 #lang-pulse
 
 open Pulse.Lib.Pervasives
-open Pulse.Lib.Trade
+open Pulse.Lib.SendableTrade
 
 module GR = Pulse.Lib.GhostReference
 
 let pledge is f v = pure (is_finite is) ** trade #is f (f ** v)
 
+let is_send_pledge is f v = Tactics.Typeclasses.solve
+
 fn introducable_pledge_aux u#a (t: Type u#a) (is: inames) (is': fin_inames)
-    (f v extra: slprop) {| inst: introducable is' (extra ** f) (f ** v) t |} (x:t) :
+    (f v extra: slprop) {| is_send extra |} {| inst: introducable is' (extra ** f) (f ** v) t |} (x:t) :
     stt_ghost unit is extra (fun _ -> pledge is' f v) = {
   intro #is (trade #is' f (f ** v)) #extra (fun _ -> x);
   fold pledge is' f v;
 }
 
 instance introducable_pledge (t: Type u#a) is (is': fin_inames)
-    f v extra {| introducable is' (extra ** f) (f ** v) t |} :
+    f v extra {| is_send extra |} {| introducable is' (extra ** f) (f ** v) t |} :
     introducable is extra (pledge is' f v) t =
   { intro_aux = introducable_pledge_aux t is is' f v extra }
 
@@ -56,7 +58,7 @@ fn pledge_sub_inv (is1:inames) (is2:fin_inames { inames_subset is1 is2 })(f:slpr
 } 
 
 ghost
-fn return_pledge (f v : slprop)
+fn return_pledge (f v : slprop) {| is_send v |}
   requires v
   ensures pledge emp_inames f v
 {
@@ -67,7 +69,7 @@ fn return_pledge (f v : slprop)
 let call #t #is #req #ens (h: unit -> stt_ghost is t req (fun x -> ens x)) = h
 
 ghost
-fn make_pledge (is:fin_inames) (f:slprop) (v:slprop) (extra:slprop)
+fn make_pledge (is:fin_inames) (f:slprop) (v:slprop) (extra:slprop) {| is_send extra |}
   (k: unit -> pledge_f #is f #extra v)
   requires extra
   ensures pledge is f v
@@ -107,7 +109,7 @@ fn squash_pledge (is:inames) (f:slprop) (v1:slprop)
 
 ghost
 fn bind_pledge (#is:inames) (#f:slprop) (#v1:slprop) (#v2:slprop)
-        (extra : slprop)
+        (extra : slprop) {| is_send extra |}
         (#is_k:inames { inames_subset is_k is })
         (k:unit -> bind_pledge_f #is #is_k f #extra v1 v2)
   requires pledge is f v1 ** extra
@@ -125,13 +127,13 @@ fn bind_pledge (#is:inames) (#f:slprop) (#v1:slprop) (#v2:slprop)
 
 ghost
 fn bind_pledge' (#is:inames) (#f:slprop) (#v1:slprop) (#v2:slprop)
-        (extra : slprop)
+        (extra : slprop) {| is_send extra |}
         (#is_k:inames { inames_subset is_k is })
         (k:unit -> bind_pledge_f' #is #is_k f #extra v1 v2)
   requires pledge is f v1 ** extra
   ensures pledge is f v2
 {
-  bind_pledge #is #f #v1 #v2 extra #is_k fn _ {
+  bind_pledge #is #f #v1 #v2 extra #_ #is_k fn _ {
     call k ()
   };
 }
@@ -204,10 +206,6 @@ fn squash_pledge'
 }
 
 
-//
-// This proof below requires inv_p to be big ...
-//
-
 (* A big chunk follows for split_pledge *)
 
 [@@no_mkeys]
@@ -300,12 +298,13 @@ fn elim_body_l1
 {
   open Pulse.Lib.GhostReference;
   assert (pure (not (mem_inv is i)));
-  with_invariants i
-  {
-    later_elim _;
-    do_elim_body_l #is #f v1 v2 r1 r2 ();
-    later_intro (inv_p is f v1 v2 r1 r2);
-  };
+  with_inv_g unit is
+    i (inv_p is f v1 v2 r1 r2)
+    (f ** (r1 |-> Frac 0.5R false))
+    (fun _ -> f ** v1)
+    fn _ {
+      do_elim_body_l #is #f v1 v2 r1 r2 ();
+    };
 }
 
 ghost
@@ -342,13 +341,14 @@ fn elim_body_r1
 {
   open Pulse.Lib.GhostReference;
   assert (pure (not (mem_inv is i)));
-  with_invariants i
-  {
-    later_elim _;
+  with_inv_g unit is
+    i (inv_p is f v1 v2 r1 r2)
+    (f ** (r2 |-> Frac 0.5R false))
+    (fun _ -> f ** v2)
+  fn _ {
     flip_invp is f v1 v2 r1 r2;
     do_elim_body_l #is #f v2 v1 r2 r1 ();
     flip_invp is f v2 v1 r2 r1;
-    later_intro (inv_p is f v1 v2 r1 r2);
   };
 }
 
@@ -381,6 +381,8 @@ fn ghost_split_pledge (#is:inames) (#f:slprop) (v1:slprop) (v2:slprop)
   as
     later_credit 1 ** later_credit 1;
 
+  admit ();
+
   intro (pledge (add_inv is i) f v1)
     #((r1 |-> Frac 0.5R false) ** later_credit 1 ** inv i (inv_p is f v1 v2 r1 r2) ** pure (not (mem_inv is i))) fn _
   {
diff --git a/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fsti b/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fsti
index 5e62a37a8..6e8eadce9 100644
--- a/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fsti
+++ b/lib/pulse/lib/pledge/Pulse.Lib.Pledge.fsti
@@ -20,13 +20,16 @@ module Pulse.Lib.Pledge
 open Pulse.Lib.Pervasives
 open Pulse.Lib.GhostSet {is_finite}
 open Pulse.Class.Introducable
+open Pulse.Lib.SendSync
 
 module T = FStar.Tactics
 
 val pledge (is:inames) (f:slprop) (v:slprop) : slprop
 
+instance val is_send_pledge is f v : is_send (pledge is f v)
+
 instance val introducable_pledge (t: Type u#a) is (is': fin_inames)
-    f v extra {| introducable is' (extra ** f) (f ** v) t |} :
+    f v extra {| is_send extra |} {| introducable is' (extra ** f) (f ** v) t |} :
     introducable is extra (pledge is' f v) t
 
 ghost
@@ -44,7 +47,7 @@ fn pledge_sub_inv (is1:inames) (is2:fin_inames { inames_subset is1 is2 }) (f v:s
 
 (* Anything that holds now holds in the future too. *)
 ghost
-fn return_pledge (f v:slprop)
+fn return_pledge (f v:slprop) {| is_send v |}
   requires v
   ensures pledge emp_inames f v
 
@@ -53,7 +56,7 @@ let pledge_f (#[T.exact (`emp_inames)] is: inames) (f: slprop) (#[T.exact (`emp)
   stt_ghost unit is (f ** extra) (fun _ -> f ** v)
 
 ghost
-fn make_pledge (is:fin_inames) (f:slprop) (v:slprop) (extra:slprop)
+fn make_pledge (is:fin_inames) (f:slprop) (v:slprop) (extra:slprop) {| is_send extra |}
   (k: unit -> pledge_f #is f #extra v)
   requires extra
   ensures pledge is f v
@@ -79,7 +82,7 @@ let bind_pledge_f (#[T.exact (`emp_inames)] is) (#[T.exact (`emp_inames)] is_k:
 // Unclear how useful/convenient this is
 ghost
 fn bind_pledge (#is:inames) (#f:slprop) (#v1:slprop) (#v2:slprop)
-        (extra : slprop)
+        (extra : slprop) {| is_send extra |}
         (#is_k:inames { inames_subset is_k is })
         (k:unit -> bind_pledge_f #is #is_k f #extra v1 v2)
   requires pledge is f v1 ** extra
@@ -95,7 +98,7 @@ let bind_pledge_f' (#[T.exact (`emp_inames)] is) (#[T.exact (`emp_inames)] is_k:
 
 ghost
 fn bind_pledge' (#is:inames) (#f:slprop) (#v1:slprop) (#v2:slprop)
-        (extra : slprop)
+        (extra : slprop) {| is_send extra |}
         (#is_k:inames { inames_subset is_k is })
         (k:unit -> bind_pledge_f' #is #is_k f #extra v1 v2)
   requires pledge is f v1 ** extra
diff --git a/lib/pulse/lib/pledge/Pulse.Lib.SendableTrade.fst b/lib/pulse/lib/pledge/Pulse.Lib.SendableTrade.fst
new file mode 100644
index 000000000..5b4bc0c02
--- /dev/null
+++ b/lib/pulse/lib/pledge/Pulse.Lib.SendableTrade.fst
@@ -0,0 +1,196 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.SendableTrade
+#lang-pulse
+
+open Pulse.Lib.Pervasives
+
+
+let trade_elim_exists (is:inames) (hyp extra concl:slprop) (inst: is_send extra) (f: unit -> trade_f #is hyp #extra concl) : slprop =
+  emp
+
+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' {
+  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
+fn intro_trade
+  (#[T.exact (`emp_inames)]is:inames)
+  (hyp concl extra:slprop) {| inst: is_send extra |}
+  (f_elim: unit -> trade_f #is hyp #extra concl)
+  requires extra
+  ensures trade #is hyp concl
+{
+  fold (trade_elim_exists is hyp extra concl inst f_elim);
+  assert (extra ** trade_elim_exists is hyp extra concl inst f_elim);
+  fold (trade #is hyp concl)
+}
+
+fn introducable_trade_aux u#a (t: Type u#a) is is'
+    hyp extra concl {| is_send extra |} {| introducable is' (extra ** hyp) concl t |} (k: t) :
+    stt_ghost unit is extra (fun _ -> trade #is' hyp concl) = {
+  intro_trade #is' hyp concl extra fn _ {
+    intro #is' concl #(extra ** hyp) (fun _ -> k);
+  }
+}
+
+instance introducable_trade (t: Type u#a) is is'
+    hyp extra concl {| is_send extra |} {| introducable is' (extra ** hyp) concl t |} :
+    introducable is extra (trade #is' hyp concl) t =
+  { intro_aux = introducable_trade_aux t is is' hyp extra concl }
+
+instance introducable_trade' (t: Type u#a) is
+    hyp extra concl {| is_send extra |} {| introducable emp_inames (extra ** hyp) concl t |} :
+    introducable is extra (hyp @==> concl) t =
+  { intro_aux = introducable_trade_aux t is emp_inames hyp extra concl }
+
+let sqeq (p : Type) (_ : squash p) : erased p =
+  FStar.IndefiniteDescription.elim_squash #p ()
+
+let psquash (a:Type u#a) : prop = squash a
+
+ghost
+fn pextract (a:Type u#5) (_:squash a)
+  requires emp
+  returns i:a
+  ensures emp
+{
+  let pf = elim_pure_explicit (psquash a);
+  let pf : squash a = FStar.Squash.join_squash pf;
+  let i = sqeq a pf;
+  let i = reveal i;
+  i
+}
+
+
+
+// ghost
+// fn deconstruct_trade (is:inames) (hyp concl: slprop)
+//   requires trade #is hyp concl
+//   returns res:(extra:slprop & is_send extra & trade_elim_t is hyp (reveal extra) concl)
+//   ensures (let (| extra, inst, _ |) = res in extra)
+// {
+//   unfold (trade #is hyp concl);
+//   with extra inst. assert (extra ** trade_elim_exists is hyp extra concl inst);
+//   unfold (trade_elim_exists is hyp (reveal extra) concl);
+//   let pf : squash (psquash (trade_elim_t is hyp (reveal extra) concl)) =
+//     elim_pure_explicit (psquash (trade_elim_t is hyp (reveal extra) concl));
+//   let pf : squash (trade_elim_t is hyp (reveal extra) concl) =
+//     FStar.Squash.join_squash pf;
+//   let f: trade_elim_t is hyp extra concl = pextract (trade_elim_t is hyp (reveal extra) concl) pf;
+//   ((| extra, inst, f |) <:
+//     (extra:slprop & is_send extra & trade_elim_t is hyp (reveal extra) concl))
+//   // let res =
+//   //   (| (extra <: erased slprop), f |) <: (p:erased slprop & trade_elim_t is hyp (reveal p) concl);
+//   // rewrite (reveal extra) as (reveal (dfst res));
+//   // res
+// }
+
+let call #t #is #req #ens (h: unit -> stt_ghost is t req (fun x -> ens x)) = h
+
+ghost
+fn elim_trade
+  (#[T.exact (`emp_inames)]is:inames)
+  (hyp concl:slprop)
+  requires trade #is hyp concl ** hyp
+  ensures concl
+  opens is
+{
+  unfold trade #is hyp concl;
+  with extra inst f. assert trade_elim_exists is hyp extra concl inst f;
+  unfold trade_elim_exists is hyp extra concl inst f;
+  let f = f;
+  call f ()
+}
+
+ghost
+fn trade_sub_inv
+  (#is1:inames)
+  (#is2:inames { inames_subset is1 is2 })
+  (hyp concl:slprop)
+  requires trade #is1 hyp concl
+  ensures trade #is2 hyp concl
+{
+  intro (trade #is2 hyp concl) #(trade #is1 hyp concl) fn _ {
+    elim_trade #is1 hyp concl
+  };
+}
+
+
+ghost
+fn trade_map
+  (#is : inames)
+  (p q r : slprop)
+  (f : unit -> stt_ghost unit emp_inames q (fun _ -> r))
+  requires trade #is p q
+  ensures  trade #is p r
+{
+  intro (trade #is p r) #(trade #is p q) fn _
+  {
+    elim_trade #is _ _;
+    f ();
+  };
+}
+
+
+ghost
+fn trade_compose
+  (#is : inames)
+  (p q r : slprop)
+  requires trade #is p q ** trade #is q r
+  ensures  trade #is p r
+{
+  intro (trade #is p r) #(trade #is p q ** trade #is q r) fn _
+  {
+    elim_trade #is p _;
+    elim_trade #is _ _;
+  };
+}
+
+ghost
+fn eq_as_trade
+  (p1 p2 : slprop)
+  requires pure (p1 == p2)
+  ensures  p2 @==> p1
+{
+  intro (p2 @==> p1) fn _{ rewrite p2 as p1 }
+}
+
+ghost
+fn rewrite_with_trade
+  (p1 p2 : slprop)
+  requires p1 ** pure (p1 == p2)
+  ensures  p2 ** (p2 @==> p1)
+{
+  eq_as_trade p1 p2;
+  rewrite p1 as p2;
+  ();
+}
diff --git a/lib/pulse/lib/pledge/Pulse.Lib.SendableTrade.fsti b/lib/pulse/lib/pledge/Pulse.Lib.SendableTrade.fsti
new file mode 100644
index 000000000..0547993e3
--- /dev/null
+++ b/lib/pulse/lib/pledge/Pulse.Lib.SendableTrade.fsti
@@ -0,0 +1,97 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.SendableTrade
+#lang-pulse
+
+open Pulse.Lib.Pervasives
+open Pulse.Class.Introducable
+open Pulse.Lib.SendSync
+
+module T = FStar.Tactics
+
+[@@erasable]
+let trade_f (#[T.exact (`emp_inames)] is: inames) (hyp: slprop) (#[T.exact (`emp)] extra: slprop) (concl: slprop) =
+  stt_ghost unit is (requires extra ** hyp) (ensures fun _ -> concl)
+
+val trade
+  (#[T.exact (`emp_inames)] is:inames)
+  ([@@@mkey] hyp:slprop)
+  ([@@@mkey] concl:slprop)
+  : slprop
+
+(* Specialized to no inames *)
+unfold
+let ( @==> ) :
+  (hyp:slprop) ->
+  (concl:slprop) ->
+  slprop
+  = trade #emp_inames
+
+instance val is_send_trade #is (p1 p2: slprop) : is_send (trade #is p1 p2)
+instance is_send_trade' (p1 p2: slprop) : is_send (p1 @==> p2) = is_send_trade p1 p2
+
+ghost
+fn intro_trade
+  (#[T.exact (`emp_inames)]is:inames)
+  (hyp concl extra:slprop) {| is_send extra |}
+  (f_elim: unit -> trade_f #is hyp #extra concl)
+  requires extra
+  ensures trade #is hyp concl
+
+instance val introducable_trade (t: Type u#a) is is'
+    hyp extra concl {| is_send extra |} {| introducable is' (extra ** hyp) concl t |} :
+    introducable is extra (trade #is' hyp concl) t
+
+instance val introducable_trade' (t: Type u#a) is
+    hyp extra concl {| is_send extra |} {| introducable emp_inames (extra ** hyp) concl t |} :
+    introducable is extra (hyp @==> concl) t
+
+val elim_trade
+  (#[T.exact (`emp_inames)] is:inames)
+  (hyp concl:slprop)
+: stt_ghost unit is
+    (trade #is hyp concl ** hyp)
+    (fun _ -> concl)
+
+ghost
+fn trade_sub_inv
+  (#is1:inames)
+  (#is2:inames { inames_subset is1 is2 })
+  (hyp concl:slprop)
+  requires trade #is1 hyp concl
+  ensures trade #is2 hyp concl
+
+ghost
+fn trade_map
+  (#is : inames)
+  (p q r : slprop)
+  (f : unit -> stt_ghost unit emp_inames q (fun _ -> r))
+  requires trade #is p q
+  ensures  trade #is p r
+
+ghost
+fn trade_compose
+  (#is : inames)
+  (p q r : slprop)
+  requires trade #is p q ** trade #is q r
+  ensures  trade #is p r
+
+ghost
+fn rewrite_with_trade
+  (p1 p2 : slprop)
+  requires p1 ** pure (p1 == p2)
+  ensures  p2 ** (p2 @==> p1)
\ No newline at end of file
diff --git a/lib/pulse/lib/pledge/Pulse.Lib.Trade.fst b/lib/pulse/lib/pledge/Pulse.Lib.Trade.fst
index 66b065d81..33dddf4d9 100644
--- a/lib/pulse/lib/pledge/Pulse.Lib.Trade.fst
+++ b/lib/pulse/lib/pledge/Pulse.Lib.Trade.fst
@@ -184,3 +184,49 @@ fn rewrite_with_trade
   rewrite p1 as p2;
   ();
 }
+
+ghost
+fn placeless_trade #is
+  (p1 p2: slprop) {| i1: placeless p1, i2: placeless p2 |}
+  : placeless (trade #is p1 p2) = l1 l2 {
+  ghost_impersonate l2 (on l1 (trade #is p1 p2)) (on l2 (trade #is p1 p2)) fn _ {
+    loc_dup l2;
+    intro (trade #is p1 p2) #(on l1 (trade #is p1 p2) ** loc l2) fn _ {
+      on_intro p1;
+      i1 l2 l1;
+      ghost_impersonate #is l1 (on l1 p1 ** on l1 (trade #is p1 p2)) (on l1 p2) fn _ {
+        on_elim p1;
+        on_elim (trade #is p1 p2);
+        elim_trade #is _ _;
+        on_intro p2
+      };
+      i2 l1 l2;
+      on_elim p2;
+      drop_ (loc l2);
+    };
+    on_intro (trade #is p1 p2);
+  };
+}
+
+ghost
+fn is_send_trade #is
+  (p1 p2: slprop) {| i1: is_send p1, i2: is_send p2 |}
+  : is_send (trade #is p1 p2) = l1 l2 {
+  ghost_impersonate l2 (on l1 (trade #is p1 p2)) (on l2 (trade #is p1 p2)) fn _ {
+    loc_dup l2;
+    intro (trade #is p1 p2) #(on l1 (trade #is p1 p2) ** loc l2) fn _ {
+      on_intro p1;
+      i1 l2 l1;
+      ghost_impersonate #is l1 (on l1 p1 ** on l1 (trade #is p1 p2)) (on l1 p2) fn _ {
+        on_elim p1;
+        on_elim (trade #is p1 p2);
+        elim_trade #is _ _;
+        on_intro p2
+      };
+      i2 l1 l2;
+      on_elim p2;
+      drop_ (loc l2);
+    };
+    on_intro (trade #is p1 p2);
+  };
+}
diff --git a/lib/pulse/lib/pledge/Pulse.Lib.Trade.fsti b/lib/pulse/lib/pledge/Pulse.Lib.Trade.fsti
index 94ee13f06..3963a1bfd 100644
--- a/lib/pulse/lib/pledge/Pulse.Lib.Trade.fsti
+++ b/lib/pulse/lib/pledge/Pulse.Lib.Trade.fsti
@@ -19,6 +19,7 @@ module Pulse.Lib.Trade
 
 open Pulse.Lib.Pervasives
 open Pulse.Class.Introducable
+open Pulse.Lib.SendSync
 
 module T = FStar.Tactics
 
@@ -99,3 +100,8 @@ fn rewrite_with_trade
   (p1 p2 : slprop)
   requires p1 ** pure (p1 == p2)
   ensures  p2 ** (p2 @==> p1)
+
+instance val placeless_trade #is (p1 p2: slprop) {| placeless p1, placeless p2 |} : placeless (trade #is p1 p2)
+instance placeless_trade' (p1 p2: slprop) {| placeless p1, placeless p2 |} : placeless (p1 @==> p2) = placeless_trade p1 p2
+instance val is_send_trade #is (p1 p2: slprop) {| is_send p1, is_send p2 |} : is_send (trade #is p1 p2)
+instance is_send_trade' (p1 p2: slprop) {| is_send p1, is_send p2 |} : is_send (p1 @==> p2) = is_send_trade p1 p2
\ No newline at end of file
diff --git a/pulse2rust/dpe/src/generated/dpe.rs b/pulse2rust/dpe/src/generated/dpe.rs
index 95d130c35..63a104bf3 100644
--- a/pulse2rust/dpe/src/generated/dpe.rs
+++ b/pulse2rust/dpe/src/generated/dpe.rs
@@ -122,30 +122,34 @@ pub fn replace_session(
             let ctr = s.st_ctr;
             let tbl = s.st_tbl;
             if sid < ctr {
-                let ret = super::pulse_lib_hashtable::lookup((), tbl, sid);
-                let tbl1 = ret.0;
-                let idx = ret.1;
-                match idx {
-                    Some(mut idx1) => {
-                        let ret1 = super::pulse_lib_hashtable::replace(
-                            (),
-                            tbl1,
-                            idx1,
-                            sid,
-                            sst,
-                            (),
-                        );
-                        let tbl2 = ret1.0;
-                        let st1 = ret1.1;
-                        let s1 = super::dpe::st {
-                            st_ctr: ctr,
-                            st_tbl: tbl2,
-                        };
-                        *mg = Some(s1);
-                        std::mem::drop(mg);
-                        st1
+                let _letpattern = super::pulse_lib_hashtable::lookup((), tbl, sid);
+                match _letpattern {
+                    (mut tbl1, mut idx) => {
+                        match idx {
+                            Some(mut idx1) => {
+                                let _letpattern1 = super::pulse_lib_hashtable::replace(
+                                    (),
+                                    tbl1,
+                                    idx1,
+                                    sid,
+                                    sst,
+                                    (),
+                                );
+                                match _letpattern1 {
+                                    (mut tbl2, mut st1) => {
+                                        let s1 = super::dpe::st {
+                                            st_ctr: ctr,
+                                            st_tbl: tbl2,
+                                        };
+                                        *mg = Some(s1);
+                                        std::mem::drop(mg);
+                                        st1
+                                    }
+                                }
+                            }
+                            None => panic!(),
+                        }
                     }
-                    None => panic!(),
                 }
             } else {
                 panic!()
diff --git a/share/pulse/examples/Dekker.fst b/share/pulse/examples/Dekker.fst
index 10bbe9e05..7b2767b06 100644
--- a/share/pulse/examples/Dekker.fst
+++ b/share/pulse/examples/Dekker.fst
@@ -96,17 +96,12 @@ ensures
   (ra |-> Frac 0.5R true) **  //a is true
   (ga |-> Frac 0.5R b)        //g is set to the return value
 ensures
-  (if b then p else emp)      //and if this returns true then we have the resource p 
+  (cond b p emp)      //and if this returns true then we have the resource p 
 {
-  later_credit_buy 1;
-  with_invariants i
-  returns _:unit
-  ensures
-    later (dekker_inv ra rb ga gb p) **
-    (ra |-> Frac 0.5R true) **
-    (ga |-> Frac 0.5R false)
-  {
-    later_elim _;
+  with_inv_stt unit emp_inames i (dekker_inv ra rb ga gb p)
+    (ra |-> Frac 0.5R false ** live ga #0.5R)
+    (fun _ -> ra |-> Frac 0.5R true ** ga |-> Frac 0.5R false)
+  fn _ {
     unfold dekker_inv;
     R.gather ra;
     write_atomic ra true;   // x := true
@@ -114,18 +109,18 @@ ensures
     GR.gather ga;
     GR.share ga;
     fold (dekker_inv ra rb ga gb p);
-    later_intro (dekker_inv ra rb ga gb p);
   };
-  later_credit_buy 1;
-  with_invariants i
-  {
-    later_elim _;
+  with_inv_stt bool emp_inames i (dekker_inv ra rb ga gb p)
+    (ra |-> Frac 0.5R true ** ga |-> Frac 0.5R false)
+    (fun b -> (ra |-> Frac 0.5R true) ** (ga |-> Frac 0.5R b) **
+      (cond b p emp))
+  fn _ {
     unfold dekker_inv;
     R.gather ra; R.share ra;
     if (read_atomic rb)
     { 
       fold (dekker_inv ra rb ga gb);
-      later_intro (dekker_inv _ _ _ _ _);
+      fold cond false p emp;
       false
     }
     else
@@ -136,7 +131,8 @@ ensures
       GR.share ga;
       intro_cond_true emp p;
       fold (dekker_inv ra rb ga gb p);
-      later_intro (dekker_inv _ _ _ _ _);
+      // later_intro (dekker_inv _ _ _ _ _);
+      fold cond true p emp;
       true
     }
   };
diff --git a/share/pulse/examples/Invariant.fst b/share/pulse/examples/Invariant.fst
index 7c44bd21c..1d0a1272c 100644
--- a/share/pulse/examples/Invariant.fst
+++ b/share/pulse/examples/Invariant.fst
@@ -34,33 +34,23 @@ fn g (i:iname)
   ensures  r ** inv i p
   opens [i]
 {
-  with_invariants i {
-    later_elim _;
+  with_inv_atomic unit emp_inames i p q (fun _ -> r) fn _ {
     f ();
-    later_intro p;
   }
 }
 
 
-#push-options "--fuel 0"
-(* Does it work without fuel? Requires the iname_list coercion
-to normalize away. *)
-
 atomic
 fn g2 (i:iname)
   requires inv i p ** q ** later_credit 1
   ensures  r ** inv i p
   opens [i]
 {
-  with_invariants i {
-    later_elim _;
+  with_inv_atomic unit emp_inames i p q (fun _ -> r) fn _ {
     f ();
-    later_intro p;
   }
 }
 
-#pop-options
-
 assume val f_ghost () : stt_ghost unit emp_inames (p ** q) (fun _ -> p ** r)
 
 
@@ -70,10 +60,8 @@ fn g_ghost (i:iname)
   ensures (r ** inv i p)
   opens [i]
 {
-  with_invariants i {
-    later_elim _;
+  with_inv_g unit emp_inames i p q (fun _ -> r) fn _ {
     f_ghost ();
-    later_intro p;
   }
 }
 
@@ -116,33 +104,24 @@ fn test2 ()
 {
   let r = Box.alloc #int 0;
   let i = new_invariant (exists* v. Box.pts_to r v);
-  with_invariants i
-    returns _:unit
-    ensures later (exists* v. pts_to r v)
-    opens [i] {
-      later_elim_timeless _;
-      atomic_write_int r 1;
-      later_intro (exists* v. pts_to r v);
+  with_inv_stt unit emp_inames i (exists* v. Box.pts_to r v) emp (fun _ -> emp) fn _ {
+    atomic_write_int r 1;
   };
   drop_ (inv i _)
 }
 
 
 // Fails as the with_invariants block is not atomic/ghost
-[@@expect_failure]
 
+[@@expect_failure [228]]
 fn test3 ()
   requires emp
   ensures emp
 {
-  let r = alloc #int 0;
+  let r = Box.alloc 0;
   let i = new_invariant (exists* v. pts_to r v);
-  with_invariants i
-    returns _:unit
-    ensures later (exists* v. pts_to r v) {
-      later_elim_storable _;
-      r := 1;
-      later_intro (exists* v. pts_to r v);
+  with_inv_stt unit emp_inames i (exists* v. pts_to r v) emp (fun _ -> emp) fn _ {
+    r := 1;
   };
   drop_ (inv i _)
 }
@@ -166,10 +145,11 @@ fn test3 ()
 atomic
 fn t0 () (i:iname)
   requires inv i emp
+  requires later_credit 1
   ensures inv i emp
   opens [i]
 {
-  with_invariants i {
+  with_inv_atomic unit emp_inames i emp emp (fun _ -> emp) fn _ {
     ()
   }
 }
@@ -190,15 +170,16 @@ fn basic_ghost ()
 
 
 (* Using invariants while claiming not to. *)
-[@@expect_failure]
+[@@expect_failure [19]]
 
 atomic
 fn t1 ()
+  requires later_credit 1
   requires inv i emp
   ensures inv i emp
   opens []
 {
-  with_invariants i {
+  with_inv_atomic unit emp_inames i emp emp (fun _ -> emp) fn _ {
     ()
   }
 }
@@ -208,11 +189,12 @@ fn t1 ()
 
 atomic
 fn t3 ()
+  requires later_credit 1
   requires inv i emp
   ensures inv i emp
   opens [i; i2]
 {
-  with_invariants i {
+  with_inv_atomic unit emp_inames i emp emp (fun _ -> emp) fn _ {
     ()
   }
 }
@@ -226,9 +208,7 @@ fn t2 ()
   ensures emp
 {
   let j = new_invariant emp;
-  with_invariants j 
-    returns _:unit
-    ensures later emp {
+  with_inv_stt unit emp_inames j emp emp (fun _ -> emp) fn _ {
     ()
   };
   drop_ (inv j _);
@@ -249,16 +229,11 @@ fn test_returns0 (i:iname) (b:bool)
   opens [i]
 {
   unfold folded_inv i;
-  with_invariants i
-    returns _:unit
-    ensures later p ** q {
-    later_elim _;
+  with_inv_atomic unit emp_inames i p emp (fun _ -> q) fn _ {
     if b {
       p_to_q ();
-      later_intro p;
     } else {
       ghost_p_to_q ();
-      later_intro p;
     }
   };
   fold folded_inv i
@@ -273,12 +248,8 @@ fn test_returns1 (i:iname)
   opens [i]
 {
   unfold folded_inv i;
-  with_invariants i
-    returns _:unit
-    ensures later p ** q {
-    later_elim _;
+  with_inv_g unit emp_inames i p emp (fun _ -> q) fn _ {
     ghost_p_to_q ();
-    later_intro p;
   };
   fold folded_inv i
 }
@@ -298,12 +269,8 @@ fn test_returns2 (i:iname)
   opens [i]
 {
   unfold folded_inv i;
-  with_invariants i
-    returns _:unit
-    ensures later pp ** q {
-    later_elim _;
+  with_inv_g unit emp_inames i p emp (fun _ -> q) fn _ {
     ghost_p_to_q ();
-    later_intro pp;
   };
   fold folded_inv i
 }
diff --git a/share/pulse/examples/PledgeArith.fst b/share/pulse/examples/PledgeArith.fst
index 274650f19..efd2b8b0e 100644
--- a/share/pulse/examples/PledgeArith.fst
+++ b/share/pulse/examples/PledgeArith.fst
@@ -28,7 +28,7 @@ fn pledge_return_now (f:slprop) (r : ref int)
   requires pts_to r 123
   ensures pledge emp_inames f (pts_to r 123)
 {
-  return_pledge f (pts_to r 123); // ideally automated
+  return_pledge f (pts_to r 123) #_; // ideally automated
 }
 
 
diff --git a/share/pulse/examples/PulseCorePaper.S2.Lock.fst b/share/pulse/examples/PulseCorePaper.S2.Lock.fst
index 75627db89..ae9db8efd 100644
--- a/share/pulse/examples/PulseCorePaper.S2.Lock.fst
+++ b/share/pulse/examples/PulseCorePaper.S2.Lock.fst
@@ -61,14 +61,12 @@ fn release (#p:slprop) (l:lock)
 requires protects l p ** p
 ensures protects l p
 {
-  later_credit_buy 1;
-  with_invariants l.i
-  { 
-    later_elim _;
+  with_inv_stt unit emp_inames l.i (lock_inv l.r p)
+    p (fun _ -> emp)
+  fn _ {
     with v. assert l.r |-> v;
     drop_ (maybe (v = 0ul) _);
     Pulse.Lib.Primitives.write_atomic_box l.r 0ul;
-    later_intro (lock_inv l.r p);
   }
 }
 
@@ -77,27 +75,22 @@ fn rec acquire #p (l:lock)
 requires protects l p
 ensures protects l p ** p
 {
-  later_credit_buy 1;
-  let retry = with_invariants l.i
-    returns retry:bool 
-    ensures later (lock_inv l.r p) ** (if retry then emp else p)
-  {
-    later_elim _;
+  let retry =
+    with_inv_stt bool emp_inames l.i (lock_inv l.r p)
+      emp (fun retry -> cond retry emp p)
+  fn _ {
     with v. assert (pts_to l.r v);
     let b = cas_box_alt l.r 0ul 1ul;
     if b {
-      assert (pure True);
-      // ^ Should not be needed! Looks like we're not eliminating
-      // pure slprops into the ctx before a rewrite.
       rewrite each v as 0ul;
-      assert p;
-      later_intro (lock_inv l.r p);
+      rewrite p as cond false emp p;
       false
     } else {
-      later_intro (lock_inv l.r p);
+      rewrite emp as cond true emp p;
       true
     }
   };
+  unfold cond;
   if retry { acquire l }
 }
 
diff --git a/share/pulse/examples/Quicksort.Task.fst b/share/pulse/examples/Quicksort.Task.fst
index 4533637ca..47fe5962a 100644
--- a/share/pulse/examples/Quicksort.Task.fst
+++ b/share/pulse/examples/Quicksort.Task.fst
@@ -23,6 +23,7 @@ module A = Pulse.Lib.Array
 module T = Pulse.Lib.Task
 open Quicksort.Base
 open Pulse.Lib.Pledge
+open Pulse.Lib.SendSync
 
 let quicksort_post a lo hi s0 lb rb : slprop =
   exists* s. (A.pts_to_range a lo hi s ** pure (pure_post_quicksort a lo hi lb rb s0 s))
@@ -53,10 +54,10 @@ fn rec t_quicksort
 
     T.share_alive p f;
 
-    T.spawn_ p #(f /. 2.0R) (fun () -> t_quicksort p #(f /. 2.0R) a lo p31 #lb #pivot);
+    T.spawn_ p #(f /. 2.0R) (fun () -> t_quicksort p #(f /. 2.0R) a lo p31 #lb #pivot #s1);
     t_quicksort p #(f /. 2.0R) a p32 hi #pivot #rb;
 
-    return_pledge (T.pool_done p) (A.pts_to_range a p31 p32 s2);
+    return_pledge (T.pool_done p) (A.pts_to_range a p31 p32 s2) #_;
     squash_pledge _ _ _;
     (* disambiguating makes this pretty inconvenient now, but it is robust at least... *)
     join_pledge (T.pool_alive #(f /. 2.0R) p ** quicksort_post a lo p31 s1 lb pivot) (A.pts_to_range a p31 p32 s2);
@@ -91,7 +92,7 @@ fn rec t_quicksort
     return_pledge (T.pool_done p) (
       T.pool_alive #f p **
       quicksort_post a lo hi s0 lb rb
-    );
+    ) #_;
   }
 }
 
diff --git a/share/pulse/examples/by-example/ParallelIncrement.fst b/share/pulse/examples/by-example/ParallelIncrement.fst
index 950acfd2d..0f23cfac2 100644
--- a/share/pulse/examples/by-example/ParallelIncrement.fst
+++ b/share/pulse/examples/by-example/ParallelIncrement.fst
@@ -186,15 +186,13 @@ fn atomic_increment_f2
 requires inv l (pts_to_refine x pred) ** qpred 'i
 ensures inv l (pts_to_refine x pred) ** qpred ('i + 1)
 {
-  later_credit_buy 1;
-  with_invariants l {
-    later_elim _;
+  with_inv_stt unit emp_inames l (pts_to_refine x pred) (qpred 'i) (fun _ -> qpred ('i + 1))
+  fn _ {
     unfold pts_to_refine;
     with v. _;
     atomic_increment x;
     f v 'i;
     fold pts_to_refine x pred;
-    later_intro (pts_to_refine x pred);
   }
 }
 
@@ -215,9 +213,12 @@ requires
      (pred (v + 1) ** qpred (vq + 1) ** pts_to x (v + 1)))
 ensures inv l (pts_to_refine x pred) ** qpred ('i + 1)
 {
-  later_credit_buy 1;
-  with_invariants l {
-    later_elim _;
+  with_inv_stt unit emp_inames l (pts_to_refine x pred)
+    (qpred 'i ** (forall* v vq.
+      (pred v ** qpred vq ** pts_to x (v + 1)) @==>
+      (pred (v + 1) ** qpred (vq + 1) ** pts_to x (v + 1))))
+    (fun _ -> qpred ('i + 1))
+  fn _ {
     unfold pts_to_refine;
     with v. _;
     atomic_increment x;
@@ -228,7 +229,6 @@ ensures inv l (pts_to_refine x pred) ** qpred ('i + 1)
                            (pred (v + 1) ** qpred (vq + 1) ** pts_to x (v + 1))) 'i;
     I.elim _ _;
     fold pts_to_refine x pred;
-    later_intro (pts_to_refine x pred);
   }
 }
 
@@ -250,14 +250,16 @@ requires
   ((exists* v. pts_to x v ** pred v) @==> invp)
 ensures inv l invp ** qpred ('i + 1)
 {
-  later_credit_buy 1;
-  with_invariants l {
-    later_elim _;
+  with_inv_stt unit emp_inames l invp
+    (qpred 'i **
+      (invp @==> (exists* v. pts_to x v ** pred v)) ** 
+      ((exists* v. pts_to x v ** pred v) @==> invp))
+    (fun _ -> qpred ('i + 1))
+  fn _ {
     I.elim invp _;
     atomic_increment x;
     f _ 'i;
     I.elim (exists* v. pts_to x v ** pred v) invp;
-    later_intro invp;
   }
 }
 
@@ -304,15 +306,12 @@ ensures inv l invp ** qpred ('i + 1)
   returns v:int
   ensures inv l invp
   {
-    later_credit_buy 1;
-    with_invariants l {
-        later_elim _;
+    with_inv_stt int emp_inames l invp emp (fun _ -> emp) fn _ {
         elim_inv ();
         with i. _;
         let v = atomic_read x;
         rewrite (pts_to x v) as (pts_to x i);
         intro_inv ();
-        later_intro invp;
         v
     }
   };
@@ -328,15 +327,11 @@ ensures inv l invp ** qpred ('i + 1)
     rewrite each (!continue) as true; // FIXME: rewrites_to goes the wrong direction?
     elim_cond_true _ _ _;
     let v = read ();
-    later_credit_buy 1;
     let next = 
-      with_invariants l
-      returns b1:bool
-      ensures later invp 
-          ** cond b1 (qpred 'i) (qpred ('i + 1))
-          ** pts_to continue true
-      {
-        later_elim _;
+      with_inv_stt bool emp_inames l invp
+        (qpred 'i)
+        (fun b1 -> cond b1 (qpred 'i) (qpred ('i + 1)))
+      fn _ {
         elim_inv ();
         with vv. assert pure (vv == !x);
         let b = cas x v (v + 1);
@@ -346,7 +341,6 @@ ensures inv l invp ** qpred ('i + 1)
           f vv 'i;
           intro_inv ();
           fold (cond false (qpred 'i) (qpred ('i + 1)));
-          later_intro invp;
           false
         }
         else
@@ -354,7 +348,6 @@ ensures inv l invp ** qpred ('i + 1)
           unfold cond;
           intro_inv ();
           fold (cond true (qpred 'i) (qpred ('i + 1)));
-          later_intro invp;
           true
         }
       };
@@ -383,14 +376,14 @@ fn atomic_increment_f6
 requires inv (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** pred v)) ** qpred 'i ** C.active c p
 ensures inv (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** pred v)) ** qpred ('i + 1) ** C.active c p
 {
-  later_credit_buy 1;
-  with_invariants (C.iname_of c) {
-    later_elim _;
+  with_inv_stt unit emp_inames (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** pred v))
+    (qpred 'i ** C.active c p)
+    (fun _ -> qpred ('i + 1) ** C.active c p)
+  fn _ {
     C.unpack_cinv_vp c;
     atomic_increment x;
     f _ 'i;
     C.pack_cinv_vp #(exists* v. pts_to x v ** pred v) c;
-    later_intro (C.cinv_vp c (exists* v. pts_to x v ** pred v));
   }
 }
 
diff --git a/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst b/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst
index 102a3ab6d..3f3c8fdca 100644
--- a/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst
@@ -45,20 +45,6 @@ ensures inv i (owns r)
 }
 //end create_invariant$
 
-//update_ref_atomic0$
-[@@expect_failure]
-atomic
-fn update_ref_atomic (r:ref U32.t) (i:iname) (v:U32.t)
-requires inv i (owns r)
-ensures inv i (owns r)
-{
-  with_invariants i {    //later (owns r)
-     unfold owns;        //cannot prove owns; only later (owns r)
-  }
-}
-//end update_ref_atomic0$
-
-
 //update_ref_atomic$
 atomic
 fn update_ref_atomic (r:ref U32.t) (i:iname) (v:U32.t)
@@ -66,34 +52,16 @@ requires inv i (owns r) ** later_credit 1
 ensures inv i (owns r)
 opens [i]
 {
-  with_invariants i {    //later (owns r) ** later_credit 1
-     later_elim _;       //ghost step: owns r
+  with_inv_atomic unit emp_inames i (owns r) emp (fun _ -> emp)
+  fn _ { // owns r
      unfold owns;        //ghost step;  exists* u. pts_to r u
      write_atomic r v;   //atomic step; pts_to r v
      fold owns;          //ghost step;  owns r
-     later_intro (owns r) //ghost step: later (owns r)
   } // inv i (owns r)
 }
 //end update_ref_atomic$
 
-//update_ref_atomic_alt$
-atomic
-fn update_ref_atomic_alt (r:ref U32.t) (i:iname) (v:U32.t)
-requires inv i (owns r)
-ensures inv i (owns r)
-opens [i]
-{
-  with_invariants i {    //later (owns r) ** later_credit 1
-     later_elim_timeless _;       //owns r
-     unfold owns;        //ghost step;  exists* u. pts_to r u
-     write_atomic r v;   //atomic step; pts_to r v
-     fold owns;          //ghost step;  owns r
-     later_intro (owns r) //later (owns r)
-  } // inv i (owns r)
-}
-//end update_ref_atomic_alt$
-
-
+[@@allow_ambiguous]
 ghost
 fn pts_to_dup_impossible u#a (#a: Type u#a) (x:ref a)
 requires pts_to x 'v ** pts_to x 'u
@@ -106,20 +74,24 @@ ensures  pts_to x 'v ** pts_to x 'u ** pure False
 
 
 //double_open_bad$
-[@@expect_failure]
-fn double_open_bad (r:ref U32.t) (i:inv (owns r))
-requires emp
+[@@expect_failure [19]]
+fn double_open_bad (r:ref U32.t) (i:iname)
+requires inv i (owns r)
 ensures pure False
 {
-    with_invariants i {
-      with_invariants i {
-        unfold owns;
-        unfold owns;
-        pts_to_dup_impossible r;
-        fold owns;
-        fold owns
-      }
-    }
+  dup (inv i (owns r)) ();
+  later_credit_buy 1;
+  with_inv_stt unit emp_inames i (owns r) (inv i (owns r) ** later_credit 1) (fun _ -> pure False) fn _ {
+    with_inv_atomic unit emp_inames i (owns r) (owns r) (fun _ -> pure False) fn _ {
+      unfold owns; with v. _;
+      unfold owns; with u. _;
+      pts_to_dup_impossible r;
+      drop_ (r |-> u);
+      fold owns r;
+    };
+    rewrite inv i (owns r) as owns r;
+  };
+  drop_ (inv i (owns r));
 }
 //end double_open_bad$
 
@@ -162,11 +134,11 @@ fn intro_readable (r:ref U32.t) (p:perm) (v:U32.t)
 ghost
 fn split_readable (r:ref U32.t) (i:iname)
 requires inv i (readable r)
+requires later_credit 1
 ensures inv i (readable r) ** readable r
 opens [i]
 {
-    with_invariants i {
-        later_elim_timeless _;
+  with_inv_g unit emp_inames i (readable r) emp (fun _ -> readable r) fn _ {
         unfold readable;
         with p v. assert (pts_to r #p v);
         share r;
@@ -175,7 +147,6 @@ opens [i]
         // fold readable;
         intro_readable r (p /. 2.0R) _;
         intro_readable r (p /. 2.0R) _;
-        later_intro (readable r)
     };
 }
 //end split_readable$
\ No newline at end of file
diff --git a/share/pulse/examples/by-example/PulseTutorial.DoubleIncrement.fst b/share/pulse/examples/by-example/PulseTutorial.DoubleIncrement.fst
index 6337cda7a..313d2f94b 100644
--- a/share/pulse/examples/by-example/PulseTutorial.DoubleIncrement.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.DoubleIncrement.fst
@@ -37,14 +37,14 @@ requires MR.snapshot mr v0     //and the value pf m,r
 ensures inv i (inv_core x mr)  //x and mr are still related
 ensures exists* v1. MR.snapshot mr v1 ** pure (v1 >= v0 + 1) //and value of mr is at least one more than it was before
 {
-    with_invariants i { //open the invariant i, so we can use it 
-        later_elim_timeless _; //a technicality opening invariants of this type
+    with_inv_stt unit emp_inames i (inv_core x mr) (MR.snapshot mr v0)
+        (fun _ -> exists* v1. MR.snapshot mr v1 ** pure (v1 >= v0 + 1))
+    fn _ { //open the invariant i, so we can use it 
         MR.recall_snapshot mr; //Ghost step: this tells us that v0 <= current value of x
         drop_ (MR.snapshot mr v0); //we don't need the snapshot of v0 anymore
         let res = incr_atomic x; //to the actual increment
         MR.update mr res; //Ghost step: update the ghost reference to the new value
         MR.take_snapshot mr #1.0R res; //Take a new snapshot of the ghost reference at the current value
-        later_intro (inv_core x mr); //a technicality to reintroduce the invariant
     }
 }
 
diff --git a/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareable.fst b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareable.fst
index 5d54dd2b5..455c6ed8a 100644
--- a/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareable.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareable.fst
@@ -44,10 +44,10 @@ ensures c.inv 0
     fold (inv_core x mr);
     let ii = new_invariant (inv_core x mr);
     with inv. assert pure (inv == (fun (i: int) ->
-        Pulse.Lib.Core.inv ii (inv_core x mr) ** MR.snapshot mr i));
+        Pulse.Lib.Inv.inv ii (inv_core x mr) ** MR.snapshot mr i));
     fn next (#_:unit) : next_f inv = i {
-        with_invariants ii {
-            later_elim_timeless _;
+        with_inv_stt int emp_inames ii (inv_core x mr) (MR.snapshot mr i)
+            (fun j -> MR.snapshot mr j ** pure (i < j)) fn _ {
             unfold inv_core;
             let res = incr_atomic_box x;
             MR.recall_snapshot mr;
@@ -55,7 +55,6 @@ ensures c.inv 0
             drop_ (MR.snapshot mr i);
             MR.take_snapshot mr #1.0R res;
             fold (inv_core);
-            later_intro (inv_core x mr);
             res
         }
     };
diff --git a/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareableFreeable.fst b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareableFreeable.fst
index 8fb789f8c..edfc5f26a 100644
--- a/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareableFreeable.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareableFreeable.fst
@@ -64,12 +64,13 @@ ensures c.inv 1.0R 0
     let ii = CI.new_cancellable_invariant (inv_core x mr);
     
     with inv. assert pure (inv == (fun p (i:int) ->
-        Pulse.Lib.Core.inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii p ** MR.snapshot mr i));
+        Pulse.Lib.Inv.inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii p ** MR.snapshot mr i));
 
     fn next (#_: unit) : next_f inv = p i {
-        later_credit_buy 1;
-        with_invariants (iname_of ii) {
-            later_elim _;
+        with_inv_stt int emp_inames (iname_of ii) (cinv_vp ii (inv_core x mr))
+            (CI.active ii p ** MR.snapshot mr i)
+            (fun j -> CI.active ii p ** MR.snapshot mr j ** pure (i < j))
+        fn _ {
             unpack_cinv_vp ii;
             unfold inv_core;
             let res = incr_atomic_box x;
@@ -79,7 +80,6 @@ ensures c.inv 1.0R 0
             MR.take_snapshot mr #1.0R res;
             fold (inv_core);
             pack_cinv_vp ii;
-            later_intro (cinv_vp ii (inv_core x mr));
             res
         }
     };
@@ -95,7 +95,7 @@ ensures c.inv 1.0R 0
     fn gather (#_: unit) : gather_f inv = p q i j {
         CI.gather #p #q ii;
         drop_ (MR.snapshot mr j);
-        drop_ (Pulse.Lib.Core.inv (iname_of ii) (cinv_vp ii (inv_core x mr)));
+        drop_ (Pulse.Lib.Inv.inv (iname_of ii) (cinv_vp ii (inv_core x mr)));
     };
 
     fn destroy (#_: unit) : destroy_f inv = i {
diff --git a/share/pulse/examples/by-example/PulseTutorial.PCMParallelIncrement.fst b/share/pulse/examples/by-example/PulseTutorial.PCMParallelIncrement.fst
index f75ebe77e..3e937ba76 100644
--- a/share/pulse/examples/by-example/PulseTutorial.PCMParallelIncrement.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.PCMParallelIncrement.fst
@@ -360,13 +360,13 @@ ensures
         (CI.cinv_vp i (contributions n initial gs r))
 opens [CI.iname_of i] //we used the invariant
 { 
-  with_invariants (CI.iname_of i)
-  {
-    later_elim _;
+  with_inv_atomic unit emp_inames (CI.iname_of i) (CI.cinv_vp i (contributions n initial gs r))
+    (can_give gs 1 ** CI.active i p)
+    (fun _ -> has_given gs 1 ** CI.active i p)
+  fn _ {
     CI.unpack_cinv_vp i;
     incr_core gs r;
     CI.pack_cinv_vp i;
-    later_intro (CI.cinv_vp i (contributions n initial gs r));
   }
 }
 
@@ -434,9 +434,9 @@ ensures
        (CI.cinv_vp ci (contributions capacity initial gs r))
 opens [CI.iname_of ci]
 {
-  with_invariants (CI.iname_of ci)
-  {
-    later_elim _;
+  with_inv_g unit emp_inames (CI.iname_of ci) (CI.cinv_vp ci (contributions capacity initial gs r))
+    (CI.active ci p) (fun _ -> has_given gs 0 ** CI.active ci p)
+  fn _ {
     CI.unpack_cinv_vp ci;
     unfold contributions;
     with u. assert (owns_tank_units gs.to_give u);
@@ -444,7 +444,6 @@ opens [CI.iname_of ci]
     fold (has_given gs 0);
     fold (contributions capacity initial gs r);
     CI.pack_cinv_vp #(contributions capacity initial gs r) ci;
-    later_intro (CI.cinv_vp ci (contributions capacity initial gs r));
   }
 }
 
diff --git a/share/pulse/examples/by-example/PulseTutorial.ParallelIncrement.fst b/share/pulse/examples/by-example/PulseTutorial.ParallelIncrement.fst
index 0589e4020..74d19fb79 100644
--- a/share/pulse/examples/by-example/PulseTutorial.ParallelIncrement.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.ParallelIncrement.fst
@@ -74,7 +74,7 @@ fn attempt (x:ref int)
 requires pts_to x 'i
 ensures exists* v. pts_to x v
 {
-  let l = L.new_lock (exists* v. pts_to x v);
+  let l = L.new_lock (exists* (v: int). pts_to x v);
   fn incr ()
   requires L.lock_alive l #0.5R (exists* v. pts_to x v)
   ensures L.lock_alive l #0.5R (exists* v. pts_to x v)
@@ -318,13 +318,15 @@ ensures inv (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) **
   returns v:int
   ensures inv (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) ** C.active c p
   {
-    with_invariants (C.iname_of c)
-    {
-        later_elim _;
+    with_inv_atomic int emp_inames (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v))
+      (C.active c p) (fun _ -> C.active c p) fn _ {
+    // with_invariants (C.iname_of c) (C)
+    // {
+    //     later_elim _;
         C.unpack_cinv_vp #p c;
         let v = atomic_read x;
         C.pack_cinv_vp #(exists* v. pts_to x v ** refine v) c;
-        later_intro (C.cinv_vp c (exists* v. pts_to x v ** refine v));
+        // later_intro (C.cinv_vp c (exists* v. pts_to x v ** refine v));
         v
     }
   };
@@ -342,16 +344,15 @@ ensures inv (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) **
     rewrite each (!continue) as true; // FIXME: rewrites_to goes in the wrong direction
     later_credit_buy 1;
     let v = read ();
-    later_credit_buy 1;
-    let next = 
-      with_invariants (C.iname_of c)
-      returns b1:bool
-      ensures later (C.cinv_vp c (exists* v. pts_to x v ** refine v))
-          ** cond b1 (aspec 'i) (aspec ('i + 1))
+    let next =
+      with_inv_stt bool emp_inames
+        (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v))
+        (C.active c p ** pts_to continue true **
+          cond (!continue) (aspec 'i) (aspec ('i + 1)))
+        (fun b1 -> cond b1 (aspec 'i) (aspec ('i + 1))
           ** pts_to continue true
-          ** C.active c p
-      {
-        later_elim _;
+          ** C.active c p)
+      fn _ {
         C.unpack_cinv_vp c;
         unfold cond;
         with vv. assert x |-> vv;
@@ -362,7 +363,6 @@ ensures inv (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) **
           f vv 'i;
           C.pack_cinv_vp #(exists* v. pts_to x v ** refine v) c;
           fold (cond false (aspec 'i) (aspec ('i + 1)));
-          later_intro (C.cinv_vp c (exists* v. pts_to x v ** refine v));
           false
         }
         else
@@ -370,7 +370,6 @@ ensures inv (C.iname_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) **
           unfold cond;
           C.pack_cinv_vp #(exists* v. pts_to x v ** refine v) c;
           fold (cond true (aspec 'i) (aspec ('i + 1)));
-          later_intro (C.cinv_vp c (exists* v. pts_to x v ** refine v));
           true
         }
       };
diff --git a/share/pulse/examples/by-example/PulseTutorial.SpinLock.fst b/share/pulse/examples/by-example/PulseTutorial.SpinLock.fst
index a71bee46f..1fda156bf 100644
--- a/share/pulse/examples/by-example/PulseTutorial.SpinLock.fst
+++ b/share/pulse/examples/by-example/PulseTutorial.SpinLock.fst
@@ -80,13 +80,9 @@ ensures lock_alive l p ** p
 //acquire_body$
 {
   unfold lock_alive;
-  later_credit_buy 1;
   let b = 
-    with_invariants l.i
-      returns b:bool
-      ensures later (lock_inv l.r p) ** maybe b p
-      opens [l.i] {
-      later_elim _;
+    with_inv_stt bool emp_inames l.i (lock_inv l.r p)
+      emp (fun b -> maybe b p) fn _ {
       unfold lock_inv;
       with vv. assert l.r |-> vv;
       let b = cas_box l.r 0ul 1ul;
@@ -97,7 +93,6 @@ ensures lock_alive l p ** p
         fold (maybe false p);
         rewrite (maybe false p) as (maybe (1ul = 0ul) p);
         fold (lock_inv l.r p);
-        later_intro (lock_inv l.r p);
         true
       }
       else
@@ -105,7 +100,6 @@ ensures lock_alive l p ** p
         elim_cond_false _ _ _;
         fold (lock_inv l.r p);
         fold (maybe false p);
-        later_intro (lock_inv l.r p);
         false
       }
     };
@@ -121,18 +115,12 @@ requires lock_alive l p ** p
 ensures lock_alive l p
 {
   unfold lock_alive;
-  later_credit_buy 1;
-  with_invariants l.i
-    returns _:unit
-    ensures later (lock_inv l.r p)
-    opens [l.i] {
-    later_elim _;
+  with_inv_stt unit emp_inames l.i (lock_inv l.r p) p (fun _ -> emp) fn _ {
     unfold lock_inv;
     write_atomic_box l.r 0ul;
     drop_ (maybe _ _); //maybe release without acquire
     fold (maybe (0ul = 0ul) p);
     fold (lock_inv l.r p);
-    later_intro (lock_inv l.r p);
   };
   fold lock_alive
 }
diff --git a/share/pulse/examples/parallel/ParallelFor.fst b/share/pulse/examples/parallel/ParallelFor.fst
index 6ada98edb..bcf0028ed 100644
--- a/share/pulse/examples/parallel/ParallelFor.fst
+++ b/share/pulse/examples/parallel/ParallelFor.fst
@@ -23,6 +23,7 @@ open Pulse.Lib.Task
 open FStar.Real
 open Pulse.Lib.Pledge
 open Pulse.Lib.OnRange
+open Pulse.Lib.SendSync
 
 module P = Pulse.Lib.Pledge
 module R = Pulse.Lib.Reference
@@ -227,8 +228,8 @@ fn rec redeem_range
 
 fn
 parallel_for
-  (pre : (nat -> slprop))
-  (post : (nat -> slprop))
+  (pre : (nat -> slprop)) {| (x:nat -> is_send (pre x)) |}
+  (post : (nat -> slprop)) {| (x:nat -> is_send (post x)) |}
   (f : (i:nat -> stt unit (pre i) (fun () -> (post i))))
   (n : pos)
   requires on_range pre 0 n
@@ -280,8 +281,8 @@ spawning sequentially. *)
 
 fn
 parallel_for_alt
-  (pre : (nat -> slprop))
-  (post : (nat -> slprop))
+  (pre : (nat -> slprop)) {| (x:nat -> is_send (pre x)) |}
+  (post : (nat -> slprop)) {| (x:nat -> is_send (post x)) |}
   (f : (i:nat -> stt unit (pre i) (fun () -> (post i))))
   (n : pos)
   requires on_range pre 0 n
@@ -378,8 +379,8 @@ fn rec funfold
 
 fn
 parallel_for_wsr
-  (pre : (nat -> slprop))
-  (post : (nat -> slprop))
+  (pre : (nat -> slprop)) {| (x:nat -> is_send (pre x)) |}
+  (post : (nat -> slprop)) {| (x:nat -> is_send (post x)) |}
   (full_pre : (nat -> slprop))
   (full_post : (nat -> slprop))
   (f : (i:nat -> stt unit (pre i) (fun () -> post i)))
@@ -407,8 +408,8 @@ val frame_stt_left
 fn rec h_for_task
   (p:pool)
   (e:perm)
-  (pre : (nat -> slprop))
-  (post : (nat -> slprop))
+  (pre : (nat -> slprop)) {| (x:nat -> is_send (pre x)) |}
+  (post : (nat -> slprop)) {| (x:nat -> is_send (post x)) |}
   (f : (i:nat -> stt unit (pre i) (fun () -> post i)))
   (lo hi : nat)
   (_:unit)
@@ -421,7 +422,7 @@ fn rec h_for_task
     for_loop pre post emp
              (fun i -> frame_stt_left emp (f i)) lo hi;
 
-    return_pledge (pool_done p) (on_range post lo hi)
+    return_pledge (pool_done p) (on_range post lo hi) #_
   } else {
     let mid = (hi+lo)/2;
     assert (pure (lo <= mid /\ mid <= hi));
@@ -482,8 +483,8 @@ val wait_pool
 
 fn
 parallel_for_hier
-  (pre : (nat -> slprop))
-  (post : (nat -> slprop))
+  (pre : (nat -> slprop)) {| (x:nat -> is_send (pre x)) |}
+  (post : (nat -> slprop)) {| (x:nat -> is_send (post x)) |}
   (f : (i:nat -> stt unit (pre i) (fun () -> (post i))))
   (n : pos)
   requires on_range pre 0 n
diff --git a/share/pulse/examples/parallel/Promises.Examples3.fst b/share/pulse/examples/parallel/Promises.Examples3.fst
index 83d0b02cc..39ac0260f 100644
--- a/share/pulse/examples/parallel/Promises.Examples3.fst
+++ b/share/pulse/examples/parallel/Promises.Examples3.fst
@@ -35,6 +35,11 @@ let inv_p : timeless_slprop =
     ** pure (v_claimed ==> v_done)
     ** pure (v_done ==> Some? v_res)
 
+instance is_send_if a b c {| ib: is_send b, ic: is_send c |} : is_send (if a then b else c) =
+  if a then ib else ic
+
+instance is_send_inv_p : is_send inv_p = Tactics.Typeclasses.solve
+
 (* Explicit introduction for inv_p, sometimes needed to disambiguate. *)
 
 ghost
@@ -61,15 +66,18 @@ let goal : slprop =
 
 
 
-atomic
+ghost
 fn proof
    (i : iname) (_:unit)
    requires inv i inv_p ** pts_to done #0.5R true ** pts_to claimed #0.5R false
+   requires later_credit 1
    ensures inv i inv_p ** pts_to done #0.5R true ** goal
    opens [i]
 {
-  with_invariants i {
-    later_elim_timeless _;
+  with_inv_g unit emp_inames i inv_p 
+    (pts_to done #0.5R true ** pts_to claimed #0.5R false)
+    (fun _ -> pts_to done #0.5R true ** goal)
+    fn _ {
     unfold inv_p;
     with (v_done : bool) v_res (v_claimed : bool).
       assert (pts_to done #0.5R v_done
@@ -116,8 +124,6 @@ fn proof
     
     drop_ (pts_to claimed #0.5R true);
 
-    later_intro inv_p;
-
     ()
   }
 }
@@ -146,10 +152,12 @@ fn setup (_:unit)
   fold inv_p;
   
   let i = new_invariant inv_p;
+  later_credit_buy 1;
   intro (pledge (add_inv emp_inames i) (pts_to done #0.5R true) goal)
-      #(inv i inv_p ** pts_to claimed #0.5R false) fn _ {
-    //cheating: (proof i) is atomic, not ghost
-    admit()
+      #(inv i inv_p ** pts_to claimed #0.5R false ** later_credit 1)
+  fn _ {
+    proof i ();
+    drop_ (inv i inv_p);
   };
 
   i
diff --git a/share/pulse/examples/parallel/TaskPool.Examples.fst b/share/pulse/examples/parallel/TaskPool.Examples.fst
index eaa49d659..a1a64e6f9 100644
--- a/share/pulse/examples/parallel/TaskPool.Examples.fst
+++ b/share/pulse/examples/parallel/TaskPool.Examples.fst
@@ -20,9 +20,13 @@ module TaskPool.Examples
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Pledge
 open Pulse.Lib.Task
+open Pulse.Lib.SendSync
 
 assume
 val qsv : nat -> slprop
+[@@Tactics.Typeclasses.tcinstance]
+assume
+val is_send_qsv n : is_send (qsv n)
 assume
 val qsc : n:nat -> stt unit emp (fun _ -> qsv n)
 
@@ -111,7 +115,6 @@ fn qs12_par (#e:perm) (p:pool)
     ()
   }
 
-
 fn qsh_par (n:nat)
   requires emp
   returns _:unit
@@ -119,7 +122,7 @@ fn qsh_par (n:nat)
 {
   let p = setup_pool 42;
   share_alive p _;
-  spawn_ p (fun () -> qs12_par p);
+  spawn_ p (fun () -> qs12_par #(1.0R/.2.0R) p);
   spawn_ p (fun () -> qsc 3);
   spawn_ p (fun () -> qsc 4);
   join_pledge #emp_inames #(pool_done p) (qsv 3) (qsv 4);
diff --git a/test/ExtractionTest.fst b/test/ExtractionTest.fst
index 81d322a76..750bf777f 100644
--- a/test/ExtractionTest.fst
+++ b/test/ExtractionTest.fst
@@ -27,12 +27,8 @@ fn test_invariants_and_later ()
   ensures emp
 {
   let i = new_invariant emp;
-  later_credit_buy 1;
-  with_invariants i
-    returns _: unit
-    ensures later emp {
-    later_elim emp;
-    later_intro emp;
+  with_inv_stt unit emp_inames i emp emp (fun _ -> emp) fn _ {
+    ()
   };
   drop_ (inv i emp);
 }
diff --git a/test/ExtractionTest.ml.expected b/test/ExtractionTest.ml.expected
index 05b749ebe..2890a0695 100644
--- a/test/ExtractionTest.ml.expected
+++ b/test/ExtractionTest.ml.expected
@@ -1,6 +1,7 @@
 open Prims
 let zero (uu___ : unit) : FStar_UInt32.t= Stdint.Uint32.zero
-let rec test_invariants_and_later (uu___ : unit) : unit= ()
+let rec test_invariants_and_later (uu___ : unit) : unit=
+  let k uu___1 uu___2 = () in let f uu___3 uu___4 = k () () in f () ()
 let rec test_read_write (x : FStar_UInt32.t Pulse_Lib_Reference.ref)
   (_'n : unit) : unit=
   let n = Pulse_Lib_Reference.read x () () in
diff --git a/test/bug-reports/Bug.Invariants.fst b/test/bug-reports/Bug.Invariants.fst
index 2777f1320..d636e5b49 100644
--- a/test/bug-reports/Bug.Invariants.fst
+++ b/test/bug-reports/Bug.Invariants.fst
@@ -101,7 +101,7 @@ requires inv i p
 returns x:bool
 ensures inv i p
 {
-    with_invariants i { 
+    with_inv_stt bool emp_inames i p emp (fun _ -> emp) fn _ {
       atomic_step_res();
     }
 }
@@ -115,11 +115,8 @@ requires inv i (pts_to x 1ul)
 returns _:U32.t
 ensures inv i (pts_to x 1ul)
 {
-    with_invariants i {
-        later_elim_timeless _;
-        let r = read_atomic x;
-        later_intro (pts_to x 1ul);
-        r
+    with_inv_stt U32.t emp_inames i (pts_to x 1ul) emp (fun _ -> emp) fn _ {
+        read_atomic x
     }
 }
 
@@ -130,14 +127,10 @@ requires inv i (pts_to x 0ul) ** pts_to y 'w
 ensures inv i (pts_to x 0ul) ** pts_to y 0ul
 {
     let n = 
-        with_invariants i
-        returns r:U32.t
-        ensures later (pts_to x 0ul) ** pure (r == 0ul) ** pts_to y 'w
-        opens [i] {
-            later_elim_timeless _;
-            let r = read_atomic x;
-            later_intro (pts_to x 0ul);
-            r
+        with_inv_stt U32.t emp_inames i (pts_to x 0ul)
+            (pts_to y 'w)
+            (fun r -> pure (r == 0ul) ** pts_to y 'w) fn _ {
+            read_atomic x
         };
     y := n;
 }
diff --git a/test/pool/domainslib/Makefile b/test/pool/domainslib/Makefile
index 760b78ede..5cdf04f18 100644
--- a/test/pool/domainslib/Makefile
+++ b/test/pool/domainslib/Makefile
@@ -35,6 +35,9 @@ dune: all_ml
 .PHONY: test
 test: run
 
+.PHONY: accept
+accept:
+
 .PHONY: run
 run: dune
 	./dune/_build/default/driver.exe
diff --git a/test/pool/domainslib/dune/Pulse_Lib_Task.ml b/test/pool/domainslib/dune/Pulse_Lib_Task.ml
index fafa10d79..e22fe4baf 100644
--- a/test/pool/domainslib/dune/Pulse_Lib_Task.ml
+++ b/test/pool/domainslib/dune/Pulse_Lib_Task.ml
@@ -74,6 +74,6 @@ let teardown_pool p =
     wait_for_empty p;
     T.teardown_pool p.p
 
-let spawn_ p () () () f =
+let spawn_ p () () () () () f =
     let _ = async p f in
     ()
diff --git a/test/pool/pulse_task/Makefile b/test/pool/pulse_task/Makefile
index 9d4fa6cdd..143928152 100644
--- a/test/pool/pulse_task/Makefile
+++ b/test/pool/pulse_task/Makefile
@@ -37,6 +37,9 @@ dune: all_ml
 .PHONY: test
 test: run
 
+.PHONY: accept
+accept:
+
 .PHONY: run
 run: dune
 	./dune/_build/default/driver.exe
diff --git a/test/pool/pulse_task/dune/Pulse_Lib_Core.ml b/test/pool/pulse_task/dune/Pulse_Lib_Core.ml
index cbb7a485e..5aa8287a2 100644
--- a/test/pool/pulse_task/dune/Pulse_Lib_Core.ml
+++ b/test/pool/pulse_task/dune/Pulse_Lib_Core.ml
@@ -1 +1 @@
-let fork () f = ignore (Domain.spawn f)
+let fork () () () f = ignore (Domain.spawn f)