From 6f49ec1331e6a776369a2e542a1b2eb6b6634320 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 9 Aug 2021 09:07:22 -0700
Subject: [PATCH] Redo Heapster Lifetime Subsumption (#1410)

* added ppInfoAddTypedExprNames to use a base name for each variable depending on its type; also removed old PPInfo-related code

* whoops, fixed an infinite loop

* implemented lifetime subsumption

* started adding a new version of lowned permissions that include a notion of contained lifetimes, along with an lfinished permission

* bugfix: there was an infinite loop that kept copying a block permission before eliminating it and would then go right back to trying to eliminate that same permission again...

* added debug output for return statements, which is long overdue

* changed implElimLLVMBlock to always only eliminate one step of a memblock permission; changed proveVarLLVMBlocks to focus first on eliminating memblock permissions on the left that overlap with but are not contained in memblock permissions on the right

* unfold defined shapes on the left when their ranges match a shape we are trying to prove on the right

* whoops, do not try to eliminate LHS block perms when we are proving an empty block perm on the right

* added a case to proveVarLLVMBlocks to detect if the right-hand side is a tagged union type where we already know from something on the left what the tag is, in which case we can avoid searching for proofs of all the disjuncts other than the one that matches that known tag

* added another special case to proveVarLLVMBlocks, to eliminate a sequence shape sh;emptysh with the empty shape when necessary

* finished updating Implication.hs with the new lowned permission form

* reorganized proveVarLLVMBlocks into two separate stages represented by two separate functions, all of which now take lists of multi-bindings instead of multi-bindings of lists

* whoops, forgot to change a shadowed variable...

* implemented a few more suggestions from Eric Mertens

* fixed an infinite loop in proving the new lowned permissions; also added helper function implPushCopyM

* updated the translation for the new lfinished permission and the modified lowned permission, along with all the new and modified rules; also removed a bunch of whitespace from a previous commit

* updated the remaining Heapster files to reflect the new form of the lowned permission

* added  parser support for lfinished perms and for lowned perms with non-empty contained lifetimes

* whoops, fixed the parser rules for an optional list of lifetimes
---
 .../Verifier/SAW/Heapster/IRTTranslation.hs   |   9 +-
 .../src/Verifier/SAW/Heapster/Implication.hs  | 445 ++++++++++--------
 .../src/Verifier/SAW/Heapster/Parser.y        |  10 +-
 .../src/Verifier/SAW/Heapster/Permissions.hs  | 127 ++---
 .../src/Verifier/SAW/Heapster/RustTypes.hs    |   6 +-
 .../Verifier/SAW/Heapster/SAWTranslation.hs   | 360 +++++++-------
 .../src/Verifier/SAW/Heapster/Token.hs        |   2 +
 .../src/Verifier/SAW/Heapster/TypeChecker.hs  |   6 +-
 .../src/Verifier/SAW/Heapster/UntypedAST.hs   |   6 +-
 9 files changed, 541 insertions(+), 430 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
index bf67bae7dd..e35364f76e 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs
@@ -154,8 +154,9 @@ instance ContainsIRTRecName (AtomicPerm a) where
   containsIRTRecName n (Perm_NamedConj _ args _) = containsIRTRecName n args
   containsIRTRecName n (Perm_LLVMFrame fperm) =
     containsIRTRecName n (map fst fperm)
-  containsIRTRecName _ (Perm_LOwned _ _) = False
+  containsIRTRecName _ (Perm_LOwned _ _ _) = False
   containsIRTRecName _ (Perm_LCurrent _) = False
+  containsIRTRecName _ Perm_LFinished = False
   containsIRTRecName n (Perm_Struct ps) = containsIRTRecName n ps
   containsIRTRecName _ (Perm_Fun _) = False
   containsIRTRecName _ (Perm_BVProp _) = False
@@ -414,9 +415,10 @@ instance IRTTyVars (AtomicPerm a) where
     [nuMP| Perm_NamedConj npn args off |] ->
       namedPermIRTTyVars mb_p npn args off
     [nuMP| Perm_LLVMFrame _ |] -> return ([], IRTVarsNil)
-    [nuMP| Perm_LOwned _ _ |] ->
+    [nuMP| Perm_LOwned _ _ _ |] ->
       throwError "lowned permission in an IRT definition!"
     [nuMP| Perm_LCurrent _ |] -> return ([], IRTVarsNil)
+    [nuMP| Perm_LFinished |] -> return ([], IRTVarsNil)
     [nuMP| Perm_Struct ps |] -> irtTyVars ps
     [nuMP| Perm_Fun _ |] ->
       throwError "fun perm in an IRT definition!"
@@ -660,9 +662,10 @@ instance IRTDescs (AtomicPerm a) where
     ([nuMP| Perm_NamedConj npn args off |], _) ->
       namedPermIRTDescs npn args off ixs
     ([nuMP| Perm_LLVMFrame _ |], _) -> return []
-    ([nuMP| Perm_LOwned _ _ |], _) ->
+    ([nuMP| Perm_LOwned _ _ _ |], _) ->
       error "lowned permission made it to IRTDesc translation"
     ([nuMP| Perm_LCurrent _ |], _) -> return []
+    ([nuMP| Perm_LFinished |], _) -> return []
     ([nuMP| Perm_Struct ps |], _) ->
       irtDescs ps ixs
     ([nuMP| Perm_Fun _ |], _) ->
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 1cb8c5fa98..b9c70eefd6 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -759,30 +759,51 @@ data SimplImpl ps_in ps_out where
   -- | Save a permission for later by splitting it into part that is in the
   -- current lifetime and part that is saved in the lifetime for later:
   --
-  -- > x:F<l,rws> * l:[l2]lcurrent * l2:lowned (ps_in -o ps_out)
-  -- >   -o x:F<l2,rws> * l2:lowned (x:F<l2,Rs>, ps_in -o x:F<l,rws>, ps_out)
+  -- > x:F<l,rws> * l:[l2]lcurrent * l2:lowned[ls] (ps_in -o ps_out)
+  -- >   -o x:F<l2,rws> * l2:lowned[ls](x:F<l2,Rs>, ps_in -o x:F<l,rws>, ps_out)
   --
-  -- Note that this rule also supports @l=always@, in which case the second
-  -- permission is just @l2:true@ (as a hack, because it has the same type)
+  -- Note that this rule also supports @l=always@, in which case the
+  -- @l:[l2]lcurrent@ permission is replaced by @l2:true@ (as a hack, because it
+  -- has the same type)
   SImpl_SplitLifetime ::
     KnownRepr TypeRepr a => ExprVar a -> LifetimeFunctor args a ->
     PermExprs args -> PermExpr LifetimeType -> ExprVar LifetimeType ->
-    LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+    [PermExpr LifetimeType] -> LOwnedPerms ps_in -> LOwnedPerms ps_out ->
     SimplImpl (RNil :> a :> LifetimeType :> LifetimeType)
     (RNil :> a :> LifetimeType)
 
-  -- | Subsume a smaller lifetime @l2@ inside a bigger lifetime @l1@, by putting
-  -- the @lowned@ permission for @l1@ inside that of @l2@:
+  -- | Subsume a smaller lifetime @l2@ inside a bigger lifetime @l1@, by adding
+  -- @l2@ to the lifetimes contained in the @lowned@ permission for @l@:
+  --
+  -- > l1:lowned[ls] (ps_in -o ps_out) -o l1:lowned[l2,ls] (ps_in -o ps_out)
+  SImpl_SubsumeLifetime :: ExprVar LifetimeType -> [PermExpr LifetimeType] ->
+                           LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+                           PermExpr LifetimeType ->
+                           SimplImpl (RNil :> LifetimeType)
+                           (RNil :> LifetimeType)
+
+  -- | Prove a lifetime @l@ is current during a lifetime @l2@ it contains:
   --
-  -- > l1:lowned (ps_in1 -o ps_out1) * l2:lowned (ps_in2 -o ps_out2)
-  -- >   -o l1:[l2]lcurrent
-  -- >      * l2:lowned (ps_in2 -o l1:lowned (ps_in1 -o ps_out1),ps_out2)
-  SImpl_SubsumeLifetime :: ExprVar LifetimeType ->
-                           LOwnedPerms ps_in1 -> LOwnedPerms ps_out1 ->
-                           ExprVar LifetimeType ->
-                           LOwnedPerms ps_in2 -> LOwnedPerms ps_out2 ->
-                           SimplImpl (RNil :> LifetimeType :> LifetimeType)
-                           (RNil :> LifetimeType :> LifetimeType)
+  -- > l1:lowned[ls1,l2,ls2] (ps_in -o ps_out)
+  -- >   -o l1:[l2]lcurrent * l1:lowned[ls1,l2,ls2] (ps_in -o ps_out)
+  SImpl_ContainedLifetimeCurrent :: ExprVar LifetimeType ->
+                                    [PermExpr LifetimeType] ->
+                                    LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+                                    PermExpr LifetimeType ->
+                                    SimplImpl (RNil :> LifetimeType)
+                                    (RNil :> LifetimeType :> LifetimeType)
+
+  -- | Remove a finshed contained lifetime from an @lowned@ permission:
+  --
+  -- > l1:lowned[ls1,l2,ls2] (ps_in -o ps_out) * l2:lfinished
+  -- >   -o l1:lowned[ls1,ls2] (ps_in -o ps_out)
+  SImpl_RemoveContainedLifetime :: ExprVar LifetimeType ->
+                                   [PermExpr LifetimeType] ->
+                                   LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+                                   ExprVar LifetimeType ->
+                                   SimplImpl
+                                   (RNil :> LifetimeType :> LifetimeType)
+                                   (RNil :> LifetimeType)
 
   -- | Weaken a lifetime in a permission from some @l@ to some @l2@ that is
   -- contained in @l@, i.e., such that @l@ is current during @l2@, assuming that
@@ -799,9 +820,10 @@ data SimplImpl ps_in ps_out where
   --
   -- > Ps1 * Ps_in' -o Ps_in                          Ps2 * Ps_out -o Ps_out'
   -- > ----------------------------------------------------------------------
-  -- > Ps1 * Ps2 * l:lowned (Ps_in -o Ps_out) -o l:lowned (Ps_in' -o Ps_out')
+  -- > Ps1 * Ps2 * l:lowned [ls](Ps_in -o Ps_out) -o l:lowned[ls] (Ps_in' -o Ps_out')
   SImpl_MapLifetime ::
-    ExprVar LifetimeType -> LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+    ExprVar LifetimeType -> [PermExpr LifetimeType] ->
+    LOwnedPerms ps_in -> LOwnedPerms ps_out ->
     LOwnedPerms ps_in' -> LOwnedPerms ps_out' ->
     DistPerms ps1 -> DistPerms ps2 ->
     LocalPermImpl (ps1 :++: ps_in') ps_in ->
@@ -810,12 +832,14 @@ data SimplImpl ps_in ps_out where
 
   -- | End a lifetime, taking in its @lowned@ permission and all the permissions
   -- required by the @lowned@ permission to end it, and returning all
-  -- permissions given back by the @lowned@ lifetime:
+  -- permissions given back by the @lowned@ lifetime along with an @lfinished@
+  -- permission asserting that @l@ has finished:
   --
-  -- > ps_in * l:lowned (ps_in -o ps_out) -o ps_out
+  -- > ps_in * l:lowned (ps_in -o ps_out) -o ps_out * l:lfinished
   SImpl_EndLifetime :: ExprVar LifetimeType ->
                        LOwnedPerms ps_in -> LOwnedPerms ps_out ->
-                       SimplImpl (ps_in :> LifetimeType) ps_out
+                       SimplImpl (ps_in :> LifetimeType)
+                       (ps_out  :> LifetimeType)
 
   -- | Reflexivity for @lcurrent@ proofs:
   --
@@ -1660,22 +1684,34 @@ simplImplIn (SImpl_LLVMArrayIsPtr x ap) =
   distPerms1 x (ValPerm_Conj [Perm_LLVMArray ap])
 simplImplIn (SImpl_LLVMBlockIsPtr x bp) =
   distPerms1 x (ValPerm_Conj [Perm_LLVMBlock bp])
-simplImplIn (SImpl_SplitLifetime x f args l l2 ps_in ps_out) =
+simplImplIn (SImpl_SplitLifetime x f args l l2 sub_ls ps_in ps_out) =
   -- If l=always then the second permission is l2:true
   let (l',l'_p) = lcurrentPerm l l2 in
-  distPerms3 x (ltFuncApply f args l) l' l'_p l2 (ValPerm_LOwned ps_in ps_out)
-simplImplIn (SImpl_SubsumeLifetime l1 ps_in1 ps_out1 l2 ps_in2 ps_out2) =
-  distPerms2 l1 (ValPerm_LOwned ps_in1 ps_out1)
-  l2 (ValPerm_LOwned ps_in2 ps_out2)
+  distPerms3 x (ltFuncApply f args l) l' l'_p
+  l2 (ValPerm_LOwned sub_ls ps_in ps_out)
+simplImplIn (SImpl_SubsumeLifetime l ls ps_in ps_out _) =
+  distPerms1 l (ValPerm_LOwned ls ps_in ps_out)
+simplImplIn (SImpl_ContainedLifetimeCurrent l ls ps_in ps_out l2) =
+  if elem l2 ls then
+    distPerms1 l (ValPerm_LOwned ls ps_in ps_out)
+  else
+    error ("simplImplIn: SImpl_ContainedLifetimeCurrent: " ++
+           "lifetime not in contained lifetimes")
+simplImplIn (SImpl_RemoveContainedLifetime l ls ps_in ps_out l2) =
+  if elem (PExpr_Var l2) ls then
+    distPerms2 l (ValPerm_LOwned ls ps_in ps_out) l2 ValPerm_LFinished
+  else
+    error ("simplImplIn: SImpl_RemoveContainedLifetime: " ++
+           "lifetime not in contained lifetimes")
 simplImplIn (SImpl_WeakenLifetime x f args l l2) =
   let (l',l'_p) = lcurrentPerm l l2 in
   distPerms2 x (ltFuncApply f args l) l' l'_p
-simplImplIn (SImpl_MapLifetime l ps_in ps_out _ _ ps1 ps2 _ _) =
-  RL.append ps1 $ DistPermsCons ps2 l $ ValPerm_LOwned ps_in ps_out
+simplImplIn (SImpl_MapLifetime l ls ps_in ps_out _ _ ps1 ps2 _ _) =
+  RL.append ps1 $ DistPermsCons ps2 l $ ValPerm_LOwned ls ps_in ps_out
 simplImplIn (SImpl_EndLifetime l ps_in ps_out) =
   case lownedPermsToDistPerms ps_in of
     Just perms_in ->
-      DistPermsCons perms_in l $ ValPerm_LOwned ps_in ps_out
+      DistPermsCons perms_in l $ ValPerm_LOwned [] ps_in ps_out
     Nothing ->
       error "simplImplIn: SImpl_EndLifetime: non-variables in input permissions"
 simplImplIn (SImpl_LCurrentRefl _) = DistPermsNil
@@ -1972,22 +2008,33 @@ simplImplOut (SImpl_LLVMArrayIsPtr x ap) =
 simplImplOut (SImpl_LLVMBlockIsPtr x bp) =
   distPerms2 x (ValPerm_Conj1 Perm_IsLLVMPtr)
   x (ValPerm_Conj [Perm_LLVMBlock bp])
-simplImplOut (SImpl_SplitLifetime x f args l l2 ps_in ps_out) =
+simplImplOut (SImpl_SplitLifetime x f args l l2 sub_ls ps_in ps_out) =
   distPerms2 x (ltFuncApply f args $ PExpr_Var l2)
-  l2 (ValPerm_LOwned
+  l2 (ValPerm_LOwned sub_ls
       (ps_in :>: ltFuncMinApplyLOP x f (PExpr_Var l2))
       (ps_out :>: ltFuncApplyLOP x f args l))
-simplImplOut (SImpl_SubsumeLifetime l1 ps_in1 _ps_out1 l2 ps_in2 ps_out2) =
-  distPerms2 l1 (ValPerm_LCurrent $ PExpr_Var l2)
-  l2 (ValPerm_LOwned ps_in2
-      (ps_out2 :>: LOwnedPermLifetime (PExpr_Var l1) ps_in1 ps_out2))
+simplImplOut (SImpl_SubsumeLifetime l ls ps_in ps_out l2) =
+  distPerms1 l (ValPerm_LOwned (l2:ls) ps_in ps_out)
+simplImplOut (SImpl_ContainedLifetimeCurrent l ls ps_in ps_out l2) =
+  if elem l2 ls then
+    distPerms2 l (ValPerm_LCurrent l2) l (ValPerm_LOwned ls ps_in ps_out)
+  else
+    error ("simplImplOut: SImpl_ContainedLifetimeCurrent: " ++
+           "lifetime not in contained lifetimes")
+simplImplOut (SImpl_RemoveContainedLifetime l ls ps_in ps_out l2) =
+  if elem (PExpr_Var l2) ls then
+    distPerms1 l (ValPerm_LOwned (delete (PExpr_Var l2) ls) ps_in ps_out)
+  else
+    error ("simplImplOut: SImpl_RemoveContainedLifetime: " ++
+           "lifetime not in contained lifetimes")
 simplImplOut (SImpl_WeakenLifetime x f args _ l2) =
   distPerms1 x (ltFuncApply f args $ PExpr_Var l2)
-simplImplOut (SImpl_MapLifetime l _ _ ps_in' ps_out' _ _ _ _) =
-  distPerms1 l $ ValPerm_LOwned ps_in' ps_out'
-simplImplOut (SImpl_EndLifetime _ _ ps_out) =
+simplImplOut (SImpl_MapLifetime l ls _ _ ps_in' ps_out' _ _ _ _) =
+  distPerms1 l $ ValPerm_LOwned ls ps_in' ps_out'
+simplImplOut (SImpl_EndLifetime l _ ps_out) =
   case lownedPermsToDistPerms ps_out of
-    Just perms_out -> perms_out
+    Just perms_out ->
+      DistPermsCons perms_out l ValPerm_LFinished
     _ -> error "simplImplOut: SImpl_EndLifetime: non-variable in output permissions"
 simplImplOut (SImpl_LCurrentRefl l) =
   distPerms1 l (ValPerm_LCurrent $ PExpr_Var l)
@@ -2221,7 +2268,7 @@ applyImpl1 _ (Impl1_ElimLLVMBlockToEq x bp) ps =
   else
     error "applyImpl1: SImpl_ElimLLVMBlockToEq: unexpected permission"
 applyImpl1 _ Impl1_BeginLifetime ps =
-  mbPermSets1 $ nu $ \l -> pushPerm l (ValPerm_LOwned MNil MNil) ps
+  mbPermSets1 $ nu $ \l -> pushPerm l (ValPerm_LOwned [] MNil MNil) ps
 applyImpl1 _ (Impl1_TryProveBVProp x prop _) ps =
   mbPermSets1 $ emptyMb $
   pushPerm x (ValPerm_Conj [Perm_BVProp prop]) ps
@@ -2366,20 +2413,29 @@ instance SubstVar PermVarSubst m =>
       SImpl_LLVMArrayIsPtr <$> genSubst s x <*> genSubst s ap
     [nuMP| SImpl_LLVMBlockIsPtr x bp |] ->
       SImpl_LLVMBlockIsPtr <$> genSubst s x <*> genSubst s bp
-    [nuMP| SImpl_SplitLifetime x f args l l2 ps_in ps_out |] ->
+    [nuMP| SImpl_SplitLifetime x f args l l2 sub_ls ps_in ps_out |] ->
       SImpl_SplitLifetime <$> genSubst s x <*> genSubst s f <*> genSubst s args
                           <*> genSubst s l <*> genSubst s l2
+                          <*> genSubst s sub_ls
                           <*> genSubst s ps_in <*> genSubst s ps_out
-    [nuMP| SImpl_SubsumeLifetime l1 ps_in1 ps_out1 l2 ps_in2 ps_out2 |] ->
-      SImpl_SubsumeLifetime <$> genSubst s l1 <*> genSubst s ps_in1
-                            <*> genSubst s ps_out1 <*> genSubst s l2
-                            <*> genSubst s ps_in2 <*> genSubst s ps_out2
+    [nuMP| SImpl_SubsumeLifetime l ls ps_in ps_out l2 |] ->
+      SImpl_SubsumeLifetime <$> genSubst s l <*> genSubst s ls
+                            <*> genSubst s ps_in <*> genSubst s ps_out
+                            <*> genSubst s l2
+    [nuMP| SImpl_ContainedLifetimeCurrent l ls ps_in ps_out l2 |] ->
+      SImpl_ContainedLifetimeCurrent <$> genSubst s l <*> genSubst s ls
+                                     <*> genSubst s ps_in <*> genSubst s ps_out
+                                     <*> genSubst s l2
+    [nuMP| SImpl_RemoveContainedLifetime l ls ps_in ps_out l2 |] ->
+      SImpl_RemoveContainedLifetime <$> genSubst s l <*> genSubst s ls
+                                    <*> genSubst s ps_in <*> genSubst s ps_out
+                                    <*> genSubst s l2
     [nuMP| SImpl_WeakenLifetime x f args l l2 |] ->
       SImpl_WeakenLifetime <$> genSubst s x <*> genSubst s f <*> genSubst s args
                            <*> genSubst s l <*> genSubst s l2
-    [nuMP| SImpl_MapLifetime l ps_in ps_out ps_in' ps_out'
+    [nuMP| SImpl_MapLifetime l ls ps_in ps_out ps_in' ps_out'
                             ps1 ps2 impl1 impl2 |] ->
-      SImpl_MapLifetime <$> genSubst s l <*> genSubst s ps_in
+      SImpl_MapLifetime <$> genSubst s l <*> genSubst s ls <*> genSubst s ps_in
                         <*> genSubst s ps_out <*> genSubst s ps_in'
                         <*> genSubst s ps_out' <*> genSubst s ps1
                         <*> genSubst s ps2 <*> genSubst s impl1
@@ -2551,12 +2607,6 @@ data ImplState vars ps =
               _implStateVars :: CruCtx vars,
               _implStatePSubst :: PartialSubst vars,
               _implStatePVarSubst :: RAssign (Compose Maybe ExprVar) vars,
-              -- FIXME HERE: remove implStateLifetimes
-              _implStateLifetimes :: [ExprVar LifetimeType],
-              -- ^ Stack of active lifetimes, where the first element is the
-              -- current lifetime (we should have an @lowned@ permission for it)
-              -- and each lifetime contains (i.e., has an @lcurrent@ permission
-              -- for) the next lifetime in the stack
               _implStateRecRecurseFlag :: RecurseFlag,
               -- ^ Whether we are recursing under a recursive permission, either
               -- on the left hand or the right hand side
@@ -2582,7 +2632,6 @@ mkImplState vars perms env info fail_prefix do_trace nameTypes =
   _implStatePerms = perms,
   _implStatePSubst = emptyPSubst vars,
   _implStatePVarSubst = RL.map (const $ Compose Nothing) (cruCtxProxies vars),
-  _implStateLifetimes = [],
   _implStateRecRecurseFlag = RecNone,
   _implStatePermEnv = env,
   _implStatePPInfo = info,
@@ -2845,59 +2894,6 @@ setPerms perms = implStatePerms .= perms
 setPerm :: ExprVar a -> ValuePerm a -> ImplM vars s r ps ps ()
 setPerm x p = implStatePerms . varPerm x .= p
 
--- | Get the current lifetime
-getCurLifetime :: ImplM vars s r ps ps (ExprVar LifetimeType)
-getCurLifetime =
-  do ls <- use implStateLifetimes
-     case ls of
-       l:_ -> pure l
-       [] -> error "getCurLifetime: no current lifetime!"
-
--- | Push a lifetime onto the lifetimes stack
-pushLifetime :: ExprVar LifetimeType -> ImplM vars s r ps ps ()
-pushLifetime l = implStateLifetimes %= (l:)
-
--- | Pop a lifetime off of the lifetimes stack
-popLifetime :: ImplM vars s r ps ps (ExprVar LifetimeType)
-popLifetime =
-  do l <- getCurLifetime
-     implStateLifetimes %= tail
-     pure l
-
--- | Push (as in 'implPushM') the permission for the current lifetime
-implPushCurLifetimePermM :: NuMatchingAny1 r => ExprVar LifetimeType ->
-                            ImplM vars s r (ps :> LifetimeType) ps ()
-implPushCurLifetimePermM l =
-  getCurLifetime >>>= \l' ->
-  (if l == l' then pure () else
-     error "implPushLifetimePermM: wrong value for the current lifetime!") >>>
-  getPerm l >>>= \p ->
-  case p of
-    ValPerm_Conj [Perm_LOwned _ _] -> implPushM l p
-    _ -> error "implPushLifetimePermM: no LOwned permission for the current lifetime!"
-
--- | Pop (as in 'implPopM') the permission for the current lifetime
-implPopCurLifetimePermM :: NuMatchingAny1 r => ExprVar LifetimeType ->
-                           ImplM vars s r ps (ps :> LifetimeType) ()
-implPopCurLifetimePermM l =
-  getCurLifetime >>>= \l' ->
-  (if l == l' then pure () else
-     error "implPopLifetimePermM: wrong value for the current lifetime!") >>>
-  getTopDistPerm l >>>= \p ->
-  case p of
-    ValPerm_Conj [Perm_LOwned _ _] -> implPopM l p
-    _ -> error "implPopLifetimePermM: no LOwned permission for the current lifetime!"
-
-{- FIXME: this should no longer be needed!
--- | Map the final return value and the current permissions
-gmapRetAndPerms :: (PermSet ps2 -> PermSet ps1) ->
-                   (PermImpl r ps1 -> PermImpl r ps2) ->
-                   ImplM vars s r ps1 ps2 ()
-gmapRetAndPerms f_perms f_impl =
-  gmapRetAndState (over implStatePerms f_perms) f_impl
--}
-
-
 -- | Look up the type of a free variable
 implGetVarType :: Name a -> ImplM vars s r ps ps (TypeRepr a)
 implGetVarType n =
@@ -3037,20 +3033,21 @@ implCatchM m1 m2 =
 -- | "Push" all of the permissions in the permission set for a variable, which
 -- should be equal to the supplied permission, after deleting those permissions
 -- from the input permission set. This is like a simple "proof" of @x:p@.
-implPushM :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
+implPushM :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
              ImplM vars s r (ps :> a) ps ()
 implPushM x p =
   implApplyImpl1 (Impl1_Push x p) (MNil :>: Impl1Cont (const $ pure ()))
 
 -- | Call 'implPushM' for multiple @x:p@ permissions
-implPushMultiM :: NuMatchingAny1 r => DistPerms ps -> ImplM vars s r ps RNil ()
+implPushMultiM :: HasCallStack => NuMatchingAny1 r =>
+                  DistPerms ps -> ImplM vars s r ps RNil ()
 implPushMultiM DistPermsNil = pure ()
 implPushMultiM (DistPermsCons ps x p) =
   implPushMultiM ps >>> implPushM x p
 
 -- | For each permission @x:p@ in a list of permissions, either prove @x:eq(x)@
 -- by reflexivity if @p=eq(x)@ or push @x:p@ if @x@ has permissions @p@
-implPushOrReflMultiM :: NuMatchingAny1 r => DistPerms ps ->
+implPushOrReflMultiM :: HasCallStack => NuMatchingAny1 r => DistPerms ps ->
                         ImplM vars s r ps RNil ()
 implPushOrReflMultiM DistPermsNil = pure ()
 implPushOrReflMultiM (DistPermsCons ps x (ValPerm_Eq (PExpr_Var x')))
@@ -3061,7 +3058,7 @@ implPushOrReflMultiM (DistPermsCons ps x p) =
 -- | Pop a permission from the top of the stack back to the primary permission
 -- for a variable, assuming that the primary permission for that variable is
 -- empty, i.e., is the @true@ permission
-implPopM :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
+implPopM :: HasCallStack => NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
             ImplM vars s r ps (ps :> a) ()
 implPopM x p =
   implApplyImpl1 (Impl1_Pop x p) (MNil :>: Impl1Cont (const $ pure ()))
@@ -3284,6 +3281,12 @@ implCopyM :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
              ImplM vars s r (ps :> a :> a) (ps :> a) ()
 implCopyM x p = implSimplM Proxy (SImpl_Copy x p)
 
+-- | Push a copyable permission using 'implPushM', copy that permission, and
+-- then pop it back to the variable permission for @x@
+implPushCopyM :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
+                 ImplM vars s r (ps :> a) ps ()
+implPushCopyM x p = implPushM x p >>> implCopyM x p >>> implPopM x p
+
 -- | Swap the top two permissions on the top of the stack
 implSwapM :: NuMatchingAny1 r => ExprVar a -> ValuePerm a ->
              ExprVar b -> ValuePerm b ->
@@ -3465,8 +3468,7 @@ implProveEqPerms (DistPermsCons ps' x (ValPerm_Eq (PExpr_Var y)))
   | x == y
   = implProveEqPerms ps' >>> introEqReflM x
 implProveEqPerms (DistPermsCons ps' x p@(ValPerm_Eq _)) =
-  implProveEqPerms ps' >>>
-  implPushM x p >>> implCopyM x p >>> implPopM x p
+  implProveEqPerms ps' >>> implPushCopyM x p
 implProveEqPerms _ = error "implProveEqPerms: non-equality permission"
 
 -- | Cast a proof of @x:p@ to one of @x:p'@ using a proof that @p=p'@
@@ -3695,20 +3697,24 @@ implBeginLifetimeM :: NuMatchingAny1 r =>
 implBeginLifetimeM =
   implApplyImpl1 Impl1_BeginLifetime
     (MNil :>: Impl1Cont (\(_ :>: n) -> pure n)) >>>= \l ->
-  implPopM l (ValPerm_LOwned MNil MNil) >>>
+  implPopM l (ValPerm_LOwned [] MNil MNil) >>>
   pure l
 
 -- | End a lifetime, assuming the top of the stack is of the form
 --
--- > ps, ps_in, l:lowned(ps_in -o ps_out)
+-- > ps_in, l:lowned(ps_in -o ps_out)
 --
--- Pop all the returned permissions @ps_out@, leaving just @ps@ on the stack.
+-- Recombine all the returned permissions @ps_out@ and @l:lfinished@, leaving
+-- just @ps@ on the stack.
 implEndLifetimeM :: NuMatchingAny1 r => Proxy ps -> ExprVar LifetimeType ->
                     LOwnedPerms ps_in -> LOwnedPerms ps_out ->
                     ImplM vars s r ps (ps :++: ps_in :> LifetimeType) ()
-implEndLifetimeM ps l ps_in ps_out@(lownedPermsToDistPerms -> Just dps_out) =
-  implSimplM ps (SImpl_EndLifetime l ps_in ps_out) >>>
-  recombinePermsPartial ps dps_out
+implEndLifetimeM ps l ps_in ps_out@(lownedPermsToDistPerms -> Just dps_out)
+  | isJust (lownedPermsToDistPerms ps_in) =
+    implSimplM ps (SImpl_EndLifetime l ps_in ps_out) >>>
+    implTraceM (\i -> pretty "Lifetime" <+>
+                      permPretty i l <+> pretty "ended") >>>
+    recombinePermsPartial ps (DistPermsCons dps_out l ValPerm_LFinished)
 implEndLifetimeM _ _ _ _ = implFailM "implEndLifetimeM: lownedPermsToDistPerms"
 
 
@@ -3723,17 +3729,68 @@ implEndLifetimeM _ _ _ _ = implFailM "implEndLifetimeM: lownedPermsToDistPerms"
 implSplitLifetimeM :: (KnownRepr TypeRepr a, NuMatchingAny1 r) =>
                       ExprVar a -> LifetimeFunctor args a ->
                       PermExprs args -> PermExpr LifetimeType ->
-                      ExprVar LifetimeType ->
+                      ExprVar LifetimeType -> [PermExpr LifetimeType] ->
                       LOwnedPerms ps_in -> LOwnedPerms ps_out ->
                       ImplM vars s r (ps :> a)
                       (ps :> a :> LifetimeType :> LifetimeType) ()
-implSplitLifetimeM x f args l l2 ps_in ps_out =
+implSplitLifetimeM x f args l l2 sub_ls ps_in ps_out =
   implTraceM (\i ->
                sep [pretty "Splitting lifetime to" <+> permPretty i l2 <> colon,
                     permPretty i (ltFuncMinApply f l)]) >>>
-  implSimplM Proxy (SImpl_SplitLifetime x f args l l2 ps_in ps_out) >>>
+  implSimplM Proxy (SImpl_SplitLifetime x f args l l2 sub_ls ps_in ps_out) >>>
   getTopDistPerm l2 >>>= implPopM l2
 
+
+-- | Subsume a smaller lifetime @l2@ inside a bigger lifetime @l1@, by adding
+-- @l2@ to the lifetimes contained in the @lowned@ permission for @l@. Assume
+-- the top of the stack is @l1:lowned[ls] (ps_in1 -o ps_out1)@, and replace that
+-- permission with @l1:lowned[l2,ls] (ps_in1 -o ps_out1)@.
+implSubsumeLifetimeM :: NuMatchingAny1 r => ExprVar LifetimeType ->
+                        [PermExpr LifetimeType] ->
+                        LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+                        PermExpr LifetimeType ->
+                        ImplM vars s r (ps :> LifetimeType)
+                        (ps :> LifetimeType) ()
+implSubsumeLifetimeM l ls ps_in ps_out l2 =
+  implSimplM Proxy (SImpl_SubsumeLifetime l ls ps_in ps_out l2)
+
+
+-- | Prove a lifetime @l@ is current during a lifetime @l2@ it contains,
+-- assuming the permission
+--
+-- > l1:lowned[ls1,l2,ls2] (ps_in -o ps_out)
+--
+-- is on top of the stack, and replacing it with @l1:[l2]lcurrent@.
+implContainedLifetimeCurrentM :: NuMatchingAny1 r => ExprVar LifetimeType ->
+                                 [PermExpr LifetimeType] ->
+                                 LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+                                 PermExpr LifetimeType ->
+                                 ImplM vars s r (ps :> LifetimeType)
+                                 (ps :> LifetimeType) ()
+implContainedLifetimeCurrentM l ls ps_in ps_out l2 =
+  implSimplM Proxy (SImpl_ContainedLifetimeCurrent l ls ps_in ps_out l2) >>>
+  implPopM l (ValPerm_LOwned ls ps_in ps_out)
+
+
+-- | Remove a finshed contained lifetime from an @lowned@ permission. Assume the
+-- permissions
+--
+-- > l1:lowned[ls] (ps_in -o ps_out) * l2:lfinished
+--
+-- are on top of the stack where @l2@ is in @ls@, and remove @l2@ from the
+-- contained lifetimes @ls@ of @l1@, popping the resulting @lowned@ permission
+-- on @l1@ off of the stack.
+implRemoveContainedLifetimeM :: NuMatchingAny1 r => ExprVar LifetimeType ->
+                                [PermExpr LifetimeType] ->
+                                LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+                                ExprVar LifetimeType ->
+                                ImplM vars s r ps
+                                (ps :> LifetimeType :> LifetimeType) ()
+implRemoveContainedLifetimeM l ls ps_in ps_out l2 =
+  implSimplM Proxy (SImpl_RemoveContainedLifetime l ls ps_in ps_out l2) >>>
+  implPopM l (ValPerm_LOwned (delete (PExpr_Var l2) ls) ps_in ps_out)
+
+
 -- | Find all lifetimes that we currently own which could, if ended, help prove
 -- the specified permissions, and return them with their @lowned@ permissions
 lifetimesThatCouldProve :: NuMatchingAny1 r => Mb vars (DistPerms ps') ->
@@ -3743,9 +3800,9 @@ lifetimesThatCouldProve mb_ps =
   do Some all_perms <- uses implStatePerms permSetAllVarPerms
      pure (RL.foldr
              (\case
-                 VarAndPerm l (ValPerm_LOwned ps_in ps_out)
+                 VarAndPerm l (ValPerm_LOwned ls ps_in ps_out)
                    | mbLift $ fmap (lownedPermsCouldProve ps_out) mb_ps ->
-                     ((l, Perm_LOwned ps_in ps_out) :)
+                     ((l, Perm_LOwned ls ps_in ps_out) :)
                  _ -> id)
              []
              all_perms)
@@ -4122,8 +4179,8 @@ getLifetimeCurrentPerms :: NuMatchingAny1 r => PermExpr LifetimeType ->
 getLifetimeCurrentPerms PExpr_Always = pure $ Some AlwaysCurrentPerms
 getLifetimeCurrentPerms (PExpr_Var l) =
   getPerm l >>= \case
-    ValPerm_LOwned ps_in ps_out ->
-      pure $ Some $ LOwnedCurrentPerms l ps_in ps_out
+    ValPerm_LOwned ls ps_in ps_out ->
+      pure $ Some $ LOwnedCurrentPerms l ls ps_in ps_out
     ValPerm_LCurrent l' ->
       getLifetimeCurrentPerms l' >>= \some_cur_perms ->
       case some_cur_perms of
@@ -4137,15 +4194,13 @@ getLifetimeCurrentPerms (PExpr_Var l) =
 proveLifetimeCurrent :: NuMatchingAny1 r => LifetimeCurrentPerms ps_l ->
                         ImplM vars s r (ps :++: ps_l) ps ()
 proveLifetimeCurrent AlwaysCurrentPerms = pure ()
-proveLifetimeCurrent (LOwnedCurrentPerms l ps_in ps_out) =
-  implPushM l (ValPerm_LOwned ps_in ps_out)
+proveLifetimeCurrent (LOwnedCurrentPerms l ls ps_in ps_out) =
+  implPushM l (ValPerm_LOwned ls ps_in ps_out)
 proveLifetimeCurrent (CurrentTransPerms cur_perms l) =
   proveLifetimeCurrent cur_perms >>>
   let l' = lifetimeCurrentPermsLifetime cur_perms
       p_l_cur = ValPerm_LCurrent l' in
-  implPushM l p_l_cur >>>
-  implCopyM l p_l_cur >>>
-  implPopM l p_l_cur
+  implPushCopyM l p_l_cur
 
 
 ----------------------------------------------------------------------
@@ -4159,15 +4214,12 @@ simplEqPerm :: NuMatchingAny1 r => ExprVar a -> PermExpr a ->
                ImplM vars s r (as :> a) (as :> a) (PermExpr a)
 simplEqPerm x e@(PExpr_Var y) =
   getPerm y >>= \case
-  p@(ValPerm_Eq e') ->
-    implPushM y p >>> implCopyM y p >>> implPopM y p >>>
-    introCastM x y p >>> pure e'
+  p@(ValPerm_Eq e') -> implPushCopyM y p >>> introCastM x y p >>> pure e'
   _ -> pure e
 simplEqPerm x e@(PExpr_LLVMOffset y off) =
   getPerm y >>= \case
   p@(ValPerm_Eq e') ->
-    implPushM y p >>> implCopyM y p >>> implPopM y p >>>
-    castLLVMPtrM y p off x >>> pure (addLLVMOffset e' off)
+    implPushCopyM y p >>> castLLVMPtrM y p off x >>> pure (addLLVMOffset e' off)
   _ -> pure e
 simplEqPerm _ e = pure e
 
@@ -4201,12 +4253,12 @@ recombinePerm' x (ValPerm_Eq (PExpr_Var y)) _
 recombinePerm' x (ValPerm_Eq e1) p@(ValPerm_Eq e2)
   | e1 == e2 = implDropM x p
 recombinePerm' x x_p@(ValPerm_Eq (PExpr_Var y)) p =
-  implPushM x x_p >>> introEqCopyM x (PExpr_Var y) >>> implPopM x x_p >>>
+  implPushCopyM x x_p >>>
   invertEqM x y >>> implSwapM x p y (ValPerm_Eq (PExpr_Var x)) >>>
   introCastM y x p >>> getPerm y >>>= \y_p -> recombinePermExpl y y_p p
 recombinePerm' x x_p@(ValPerm_Eq (PExpr_LLVMOffset y off)) (ValPerm_Conj ps) =
-  implPushM x x_p >>> introEqCopyM x (PExpr_LLVMOffset y off) >>>
-  implPopM x x_p >>> implSimplM Proxy (SImpl_InvertLLVMOffsetEq x off y) >>>
+  implPushCopyM x x_p >>>
+  implSimplM Proxy (SImpl_InvertLLVMOffsetEq x off y) >>>
   implSwapM x (ValPerm_Conj ps) y (ValPerm_Eq
                                    (PExpr_LLVMOffset x (bvNegate off))) >>>
   castLLVMPtrM x (ValPerm_Conj ps) (bvNegate off) y >>>
@@ -4330,8 +4382,8 @@ recombineLifetimeCurrentPerms :: NuMatchingAny1 r =>
                                  LifetimeCurrentPerms ps_l ->
                                  ImplM vars s r ps (ps :++: ps_l) ()
 recombineLifetimeCurrentPerms AlwaysCurrentPerms = pure ()
-recombineLifetimeCurrentPerms (LOwnedCurrentPerms l ps_in ps_out) =
-  recombinePermExpl l ValPerm_True (ValPerm_LOwned ps_in ps_out)
+recombineLifetimeCurrentPerms (LOwnedCurrentPerms l ls ps_in ps_out) =
+  recombinePermExpl l ValPerm_True (ValPerm_LOwned ls ps_in ps_out)
 recombineLifetimeCurrentPerms (CurrentTransPerms cur_perms l) =
   implDropM l (ValPerm_LCurrent $ lifetimeCurrentPermsLifetime cur_perms) >>>
   recombineLifetimeCurrentPerms cur_perms
@@ -4567,13 +4619,19 @@ proveVarLifetimeFunctor' x f args l mb_l psubst = case mbMatch mb_l of
     | Right l2 <- mbNameBoundP mb_z ->
       getPerm l2 >>= \case
 
-        -- If we have l2:lowned ps, prove l:[l2]lcurrent * l2:lowned ps and then
-        -- split the lifetime
-        ValPerm_LOwned ps_in ps_out ->
+        -- If we have l2:lowned ps, prove l:[l2]lcurrent * l2:lowned ps' for
+        -- some ps' and then split the lifetime of x. Note that, in proving
+        -- l:[l2]lcurrent, we can change the lowned permission for l2,
+        -- specifically if we subsume l1 into l2.
+        ValPerm_LOwned _ _ _ ->
           let (l',l'_p) = lcurrentPerm l l2 in
           proveVarImplInt l' (fmap (const l'_p) mb_z) >>>
-          implPushM l2 (ValPerm_LOwned ps_in ps_out) >>>
-          implSplitLifetimeM x f args l l2 ps_in ps_out
+          getPerm l2 >>>= \case
+            l2_p@(ValPerm_LOwned sub_ls ps_in ps_out) ->
+              implPushM l2 l2_p >>>
+              implSplitLifetimeM x f args l l2 sub_ls ps_in ps_out
+            _ -> error ("proveVarLifetimeFunctor: unexpected error: "
+                        ++ "l2 lost its lowned perms")
 
         -- Otherwise, prove l:[l2]lcurrent and weaken the lifetime
         _ ->
@@ -4681,24 +4739,6 @@ solveForPermListImpl ps_l mb_ps = case mbMatch mb_ps of
          needed2 <- solveForPermListImpl ps_l mb_ps_r
          pure (apSomeRAssign needed1 needed2)
 
-  -- If the RHS is an lowned perm that is in the LHS, return nothing
-  --
-  -- FIXME HERE: recursively call solveForPermListImpl on the the lists of
-  -- permissions in the lifetimes
-  [nuMP| mb_ps_r :>: LOwnedPermLifetime (PExpr_Var mb_l) _ _ |]
-    | Right l <- mbNameBoundP mb_l
-    , RL.foldr (\lop rest ->
-                 case lop of
-                   LOwnedPermLifetime (PExpr_Var l') _ _
-                     | l == l' -> True
-                   _ -> rest) False ps_l ->
-      solveForPermListImpl ps_l mb_ps_r
-
-  -- If the RHS is an lowned perm not in the LHS, return the RHS
-  [nuMP| mb_ps_r :>: LOwnedPermLifetime (PExpr_Var mb_l) mb_ps_in mb_ps_out |] ->
-    apSomeRAssign (neededPerms1 mb_l (mbMap2 ValPerm_LOwned mb_ps_in mb_ps_out)) <$>
-    solveForPermListImpl ps_l mb_ps_r
-
   -- Otherwise, we don't know what to do, so do nothing and return
   _ ->
     pure (Some MNil)
@@ -6183,8 +6223,16 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
       proveEq fperms mb_fperms >>>= \eqp ->
       implCastPermM x (fmap (ValPerm_Conj1 . Perm_LLVMFrame) eqp)
 
-  [nuMP| Perm_LOwned mb_ps_inR mb_ps_outR |]
-    | [Perm_LOwned ps_inL ps_outL] <- ps ->
+  -- FIXME HERE: eventually we should handle lowned permissions on the right
+  -- with arbitrary contained lifetimes, by equalizing the two sides
+  [nuMP| Perm_LOwned [] _ _ |]
+    | [Perm_LOwned ls@(PExpr_Var l2:_) ps_in ps_out] <- ps ->
+      implEndLifetimeRecM l2 >>>
+      implRemoveContainedLifetimeM x ls ps_in ps_out l2 >>>
+      proveVarImplInt x (fmap ValPerm_Conj1 mb_p)
+
+  [nuMP| Perm_LOwned [] mb_ps_inR mb_ps_outR |]
+    | [Perm_LOwned [] ps_inL ps_outL] <- ps ->
 
       -- First, simplify both sides using any current equality permissions. This
       -- just builds the equality proofs and computes the new LHS and RHS, but
@@ -6227,7 +6275,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
       getPSubst >>>= \psubst ->
       let eqp_R =
             fmap (\(mb_ps_in,mb_ps_out) ->
-                   ValPerm_LOwned
+                   ValPerm_LOwned []
                    (partialSubstForce psubst mb_ps_in "proveVarAtomicImpl")
                    (partialSubstForce psubst mb_ps_out "proveVarAtomicImpl"))
             eqp_mb_psR in
@@ -6246,8 +6294,8 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
       -- lowned permissions and casting it, and then cast the result
       implPushM x (ValPerm_Conj ps) >>>
       implCastPermM x (fmap (\(ps_in,ps_out) ->
-                              ValPerm_LOwned ps_in ps_out) eqp_psL) >>>
-      implSimplM Proxy (SImpl_MapLifetime x ps_inL' ps_outL' ps_inR' ps_outR'
+                              ValPerm_LOwned [] ps_in ps_out) eqp_psL) >>>
+      implSimplM Proxy (SImpl_MapLifetime x [] ps_inL' ps_outL' ps_inR' ps_outR'
                         ps1 ps2 impl_in impl_out) >>>
       implCastPermM x (someEqProofSym eqp_R)
 
@@ -6261,8 +6309,16 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
       [Perm_LCurrent (PExpr_Var l)] ->
         proveVarImplInt l (fmap ValPerm_Conj1 mb_p) >>>
         implSimplM Proxy (SImpl_LCurrentTrans x l l')
+      [Perm_LOwned ls ps_in ps_out]
+        | elem l' ls -> implContainedLifetimeCurrentM x ls ps_in ps_out l'
+      [Perm_LOwned ls ps_in ps_out] ->
+        implSubsumeLifetimeM x ls ps_in ps_out l' >>>
+        implContainedLifetimeCurrentM x (l':ls) ps_in ps_out l'
       _ -> proveVarAtomicImplUnfoldOrFail x ps mb_p
 
+  [nuMP| Perm_LFinished |] ->
+    implPopM x (ValPerm_Conj ps) >>> implEndLifetimeRecM x
+
   -- If we have a struct permission on the left, eliminate it to a sequence of
   -- variables and prove the required permissions for each variable
   [nuMP| Perm_Struct mb_str_ps |]
@@ -6891,6 +6947,35 @@ localProveVars ps_in ps_out =
 -- * External Entrypoints to the Implication Prover
 ----------------------------------------------------------------------
 
+-- | End a lifetime and, recursively, all lifetimes it contains, assuming that
+-- @lowned@ permissions are held for all of those lifetimes. For each lifetime
+-- that is ended, prove its required input permissions and recombine the
+-- resulting output permissions. If a lifetime has already ended, do nothing.
+-- Leave an @lfinished@ permission for that lifetime on the top of the stack.
+implEndLifetimeRecM :: NuMatchingAny1 r => ExprVar LifetimeType ->
+                       ImplM vars s r (ps :> LifetimeType) ps ()
+implEndLifetimeRecM l =
+  getPerm l >>>= \case
+  p@ValPerm_LFinished -> implPushCopyM l p
+  p@(ValPerm_LOwned [] ps_in ps_out)
+    | Just dps_in <- lownedPermsToDistPerms ps_in ->
+      mbVarsM dps_in >>>= \mb_dps_in ->
+      -- NOTE: we are assuming that l's permission, p, will not change during
+      -- this recursive call to the prover, which should be safe
+      proveVarsImplAppendInt mb_dps_in >>>
+      implPushM l p >>> implEndLifetimeM Proxy l ps_in ps_out >>>
+      implPushCopyM l ValPerm_LFinished
+  p@(ValPerm_LOwned ((asVar -> Just l') : ls) ps_in ps_out) ->
+    implPushM l p >>>
+    implEndLifetimeRecM l' >>>
+    implRemoveContainedLifetimeM l ls ps_in ps_out l' >>>
+    implEndLifetimeRecM l
+  _ ->
+    implTraceM (\i ->
+                 pretty "implEndLifetimeRecM: could not end lifetime: " <>
+                 permPretty i l) >>>= implFailM
+
+
 -- | Prove a list of existentially-quantified distinguished permissions, adding
 -- those proofs to the top of the stack. In the case that a the variable itself
 -- whose permissions are being proved is existentially-quantified --- that is,
@@ -6901,26 +6986,18 @@ proveVarsImplAppend :: NuMatchingAny1 r => ExDistPerms vars ps ->
                        ImplM vars s r (ps_in :++: ps) ps_in ()
 proveVarsImplAppend mb_ps =
   use implStatePerms >>>= \(_ :: PermSet ps_in) ->
-  let prx :: Proxy ps_in = Proxy in
   lifetimesThatCouldProve mb_ps >>>= \ls_ps ->
   foldr1 implCatchM
   ((proveVarsImplAppendInt mb_ps)
    :
    flip map ls_ps
-   (\case
-       (l,l_p@(Perm_LOwned ps_in@(lownedPermsToDistPerms ->
-                                  Just dps_in) ps_out)) ->
-         implTraceM (\i ->
-                      sep [pretty "Ending lifetime" <+> permPretty i l,
-                           pretty "in order to prove:",
-                           permPretty i mb_ps]) >>>
-         proveVarsImplAppendInt (fmap (const dps_in) mb_ps) >>>
-         implPushM l (ValPerm_Conj1 l_p) >>>
-         implEndLifetimeM prx l ps_in ps_out >>>
-         implTraceM (\i -> pretty "Lifetime" <+> permPretty i l
-                           <+> pretty "ended") >>>
-         proveVarsImplAppend mb_ps
-       _ -> error "proveVarsImplAppend: unexpected lifetimesThatCouldProve result"))
+   (\(l,_) ->
+     implTraceM (\i ->
+                  sep [pretty "Ending lifetime" <+> permPretty i l,
+                       pretty "in order to prove:",
+                       permPretty i mb_ps]) >>>
+     implEndLifetimeRecM l >>> implDropM l ValPerm_LFinished >>>
+     proveVarsImplAppend mb_ps))
 
 -- | Prove a list of existentially-quantified distinguished permissions and put
 -- those proofs onto the stack. This is the same as 'proveVarsImplAppend' except
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y
index 6d2bcd39ce..643b9fcefc 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y
@@ -66,6 +66,7 @@ import Verifier.SAW.Heapster.UntypedAST
 'lifetime'      { Located $$ TLifetime                  }
 'lowned'        { Located $$ TLOwned                    }
 'lcurrent'      { Located $$ TLCurrent                  }
+'lfinished'     { Located $$ TLFinished                 }
 'rwmodality'    { Located $$ TRWModality                }
 'permlist'      { Located $$ TPermList                  }
 'struct'        { Located $$ TStruct                    }
@@ -179,9 +180,10 @@ expr ::                                         { AstExpr }
                                                 { ExPtr (pos $2) $1 $5 $7 Nothing $10 }
 
   | 'shape' '(' expr ')'                        { ExShape (pos $1) $3}
-  | 'lowned' '(' list(varExpr) '-o' list1(varExpr) ')'
-                                                { ExLOwned (pos $1) $3 $5}
+  | 'lowned' lifetimes '(' list(varExpr) '-o' list1(varExpr) ')'
+                                                { ExLOwned (pos $1) $2 $4 $6}
   | lifetime 'lcurrent'                         { ExLCurrent (pos $2) $1 }
+  | 'lfinished'                                 { ExLFinished (pos $1) }
 
 -- BV Props (Value Permissions)
 
@@ -223,6 +225,10 @@ lifetime ::                                     { Maybe AstExpr         }
   :                                             { Nothing               }
   | '[' expr ']'                                { Just $2               }
 
+lifetimes ::                                    { [AstExpr]             }
+  :                                             { []                    }
+  | '[' list(expr) ']'                          { $2                    }
+
 llvmFieldPermArray ::                           { ArrayPerm             }
   : lifetime '(' expr ',' expr ',' expr ')' '|->' expr
                                                 { ArrayPerm (pos $9) $1 $3 $5 (Just $7) $10 }
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index ffb297e65d..7e0c779ac5 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -1409,12 +1409,18 @@ data AtomicPerm (a :: CrucibleType) where
   -- these are a form of permission implication, so we write lifetime ownership
   -- permissions as @lowned(Pin -o Pout)@. Intuitively, @Pin@ must be given back
   -- before the lifetime is ended, and @Pout@ is returned afterwards.
-  Perm_LOwned :: LOwnedPerms ps_in -> LOwnedPerms ps_out ->
+  -- Additionally, a lifetime may contain some other lifetimes, meaning the all
+  -- must end before the current one can be ended.
+  Perm_LOwned :: [PermExpr LifetimeType] ->
+                 LOwnedPerms ps_in -> LOwnedPerms ps_out ->
                  AtomicPerm LifetimeType
 
   -- | Assertion that a lifetime is current during another lifetime
   Perm_LCurrent :: PermExpr LifetimeType -> AtomicPerm LifetimeType
 
+  -- | Assertion that a lifetime has finished
+  Perm_LFinished :: AtomicPerm LifetimeType
+
   -- | A struct permission = a sequence of permissions for each field
   Perm_Struct :: RAssign ValuePerm (CtxToRList ctx) ->
                  AtomicPerm (StructType ctx)
@@ -1498,11 +1504,12 @@ pattern ValPerm_LLVMBlockShape sh <- ValPerm_Conj [Perm_LLVMBlockShape sh]
     ValPerm_LLVMBlockShape sh = ValPerm_Conj [Perm_LLVMBlockShape sh]
 
 -- | A single @lowned@ permission
-pattern ValPerm_LOwned :: () => (a ~ LifetimeType) =>
+pattern ValPerm_LOwned :: () => (a ~ LifetimeType) => [PermExpr LifetimeType] ->
                           LOwnedPerms ps_in -> LOwnedPerms ps_out -> ValuePerm a
-pattern ValPerm_LOwned ps_in ps_out <- ValPerm_Conj [Perm_LOwned ps_in ps_out]
+pattern ValPerm_LOwned ls ps_in ps_out <- ValPerm_Conj [Perm_LOwned
+                                                        ls ps_in ps_out]
   where
-    ValPerm_LOwned ps_in ps_out = ValPerm_Conj [Perm_LOwned ps_in ps_out]
+    ValPerm_LOwned ls ps_in ps_out = ValPerm_Conj [Perm_LOwned ls ps_in ps_out]
 
 -- | A single @lcurrent@ permission
 pattern ValPerm_LCurrent :: () => (a ~ LifetimeType) =>
@@ -1511,6 +1518,12 @@ pattern ValPerm_LCurrent l <- ValPerm_Conj [Perm_LCurrent l]
   where
     ValPerm_LCurrent l = ValPerm_Conj [Perm_LCurrent l]
 
+-- | A single @lfinished@ permission
+pattern ValPerm_LFinished :: () => (a ~ LifetimeType) => ValuePerm a
+pattern ValPerm_LFinished <- ValPerm_Conj [Perm_LFinished]
+  where
+    ValPerm_LFinished = ValPerm_Conj [Perm_LFinished]
+
 -- | A sequence of value permissions
 {-
 data ValuePerms as where
@@ -1696,9 +1709,6 @@ data LOwnedPerm a where
                      LOwnedPerm (LLVMPointerType w)
   LOwnedPermBlock :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) ->
                      LLVMBlockPerm w -> LOwnedPerm (LLVMPointerType w)
-  LOwnedPermLifetime :: PermExpr LifetimeType ->
-                        LOwnedPerms ps_in -> LOwnedPerms ps_out ->
-                        LOwnedPerm LifetimeType
 
 -- | A sequence of 'LOwnedPerm's
 type LOwnedPerms = RAssign LOwnedPerm
@@ -1715,13 +1725,6 @@ instance TestEquality LOwnedPerm where
     , e1 == e2 && bp1 == bp2
     = Just Refl
   testEquality (LOwnedPermBlock _ _) _ = Nothing
-  testEquality (LOwnedPermLifetime e1 ps_in1 ps_out1)
-    (LOwnedPermLifetime e2 ps_in2 ps_out2)
-    | Just Refl <- testEquality ps_in1 ps_in2
-    , Just Refl <- testEquality ps_out1 ps_out2
-    , e1 == e2
-    = Just Refl
-  testEquality (LOwnedPermLifetime _ _ _) _ = Nothing
 
 instance Eq (LOwnedPerm a) where
   lop1 == lop2 | Just Refl <- testEquality lop1 lop2 = True
@@ -1736,8 +1739,6 @@ lownedPermExprAndPerm (LOwnedPermField e fp) =
   ExprAndPerm e $ ValPerm_LLVMField fp
 lownedPermExprAndPerm (LOwnedPermBlock e bp) =
   ExprAndPerm e $ ValPerm_LLVMBlock bp
-lownedPermExprAndPerm (LOwnedPermLifetime e ps_in ps_out) =
-  ExprAndPerm e $ ValPerm_LOwned ps_in ps_out
 
 -- | Convert an 'LOwnedPerm' to a variable plus permission, if possible
 lownedPermVarAndPerm :: LOwnedPerm a -> Maybe (VarAndPerm a)
@@ -1752,8 +1753,6 @@ varAndPermLOwnedPerm (VarAndPerm x (ValPerm_LLVMField fp)) =
   Just $ LOwnedPermField (PExpr_Var x) fp
 varAndPermLOwnedPerm (VarAndPerm x (ValPerm_LLVMBlock bp)) =
   Just $ LOwnedPermBlock (PExpr_Var x) bp
-varAndPermLOwnedPerm (VarAndPerm x (ValPerm_LOwned ps_in ps_out)) =
-  Just $ LOwnedPermLifetime (PExpr_Var x) ps_in ps_out
 varAndPermLOwnedPerm _ = Nothing
 
 -- | Get the expression part of an 'LOwnedPerm'
@@ -2048,6 +2047,14 @@ asVarOffset (PExpr_Var x) = Just (x, NoPermOffset)
 asVarOffset (PExpr_LLVMOffset x off) = Just (x, LLVMPermOffset off)
 asVarOffset _ = Nothing
 
+-- | Convert an expression to a variable if possible
+asVar :: PermExpr a -> Maybe (ExprVar a)
+asVar e
+  | Just (x,off) <- asVarOffset e
+  , offsetsEq off NoPermOffset =
+    Just x
+asVar _ = Nothing
+
 -- | Negate a 'PermOffset'
 negatePermOffset :: PermOffset a -> PermOffset a
 negatePermOffset NoPermOffset = NoPermOffset
@@ -2343,8 +2350,8 @@ data LifetimeCurrentPerms ps_l where
   AlwaysCurrentPerms :: LifetimeCurrentPerms RNil
   -- | A variable @l@ that is @lowned@ is current, requiring perms
   --
-  -- > l:lowned(ps_in -o ps_out)
-  LOwnedCurrentPerms :: ExprVar LifetimeType ->
+  -- > l:lowned[ls](ps_in -o ps_out)
+  LOwnedCurrentPerms :: ExprVar LifetimeType -> [PermExpr LifetimeType] ->
                         LOwnedPerms ps_in -> LOwnedPerms ps_out ->
                         LifetimeCurrentPerms (RNil :> LifetimeType)
 
@@ -2359,14 +2366,14 @@ data LifetimeCurrentPerms ps_l where
 lifetimeCurrentPermsLifetime :: LifetimeCurrentPerms ps_l ->
                                 PermExpr LifetimeType
 lifetimeCurrentPermsLifetime AlwaysCurrentPerms = PExpr_Always
-lifetimeCurrentPermsLifetime (LOwnedCurrentPerms l _ _) = PExpr_Var l
+lifetimeCurrentPermsLifetime (LOwnedCurrentPerms l _ _ _) = PExpr_Var l
 lifetimeCurrentPermsLifetime (CurrentTransPerms _ l) = PExpr_Var l
 
 -- | Convert a 'LifetimeCurrentPerms' to the 'DistPerms' it represent
 lifetimeCurrentPermsPerms :: LifetimeCurrentPerms ps_l -> DistPerms ps_l
 lifetimeCurrentPermsPerms AlwaysCurrentPerms = DistPermsNil
-lifetimeCurrentPermsPerms (LOwnedCurrentPerms l ps_in ps_out) =
-  DistPermsCons DistPermsNil l $ ValPerm_LOwned ps_in ps_out
+lifetimeCurrentPermsPerms (LOwnedCurrentPerms l ls ps_in ps_out) =
+  DistPermsCons DistPermsNil l $ ValPerm_LOwned ls ps_in ps_out
 lifetimeCurrentPermsPerms (CurrentTransPerms cur_ps l) =
   DistPermsCons (lifetimeCurrentPermsPerms cur_ps) l $
   ValPerm_Conj1 $ Perm_LCurrent $ lifetimeCurrentPermsLifetime cur_ps
@@ -2376,7 +2383,7 @@ mbLifetimeCurrentPermsProxies :: Mb ctx (LifetimeCurrentPerms ps_l) ->
                                  RAssign Proxy ps_l
 mbLifetimeCurrentPermsProxies mb_l = case mbMatch mb_l of
   [nuMP| AlwaysCurrentPerms |] -> MNil
-  [nuMP| LOwnedCurrentPerms _ _ _ |] -> MNil :>: Proxy
+  [nuMP| LOwnedCurrentPerms _ _ _ _ |] -> MNil :>: Proxy
   [nuMP| CurrentTransPerms cur_ps _ |] ->
     mbLifetimeCurrentPermsProxies cur_ps :>: Proxy
 
@@ -2490,13 +2497,15 @@ instance Eq (AtomicPerm a) where
   (Perm_LLVMBlockShape _) == _ = False
   (Perm_LLVMFrame frame1) == (Perm_LLVMFrame frame2) = frame1 == frame2
   (Perm_LLVMFrame _) == _ = False
-  (Perm_LOwned ps_in1 ps_out1) == (Perm_LOwned ps_in2 ps_out2)
+  (Perm_LOwned ls1 ps_in1 ps_out1) == (Perm_LOwned ls2 ps_in2 ps_out2)
     | Just Refl <- testEquality ps_in1 ps_in2
     , Just Refl <- testEquality ps_out1 ps_out2
-    = True
-  (Perm_LOwned _ _) == _ = False
+    = ls1 == ls2
+  (Perm_LOwned _ _ _) == _ = False
   (Perm_LCurrent e1) == (Perm_LCurrent e2) = e1 == e2
   (Perm_LCurrent _) == _ = False
+  Perm_LFinished == Perm_LFinished = True
+  Perm_LFinished == _ = False
   (Perm_Struct ps1) == (Perm_Struct ps2) = ps1 == ps2
   (Perm_Struct _) == _ = False
   (Perm_Fun fperm1) == (Perm_Fun fperm2)
@@ -2646,12 +2655,16 @@ instance PermPretty (AtomicPerm a) where
   permPrettyM (Perm_LLVMFrame fperm) =
     do pps <- mapM (\(e,i) -> (<> (colon <> pretty i)) <$> permPrettyM e) fperm
        return (pretty "llvmframe" <+> ppEncList False pps)
-  permPrettyM (Perm_LOwned ps_in ps_out) =
+  permPrettyM (Perm_LOwned ls ps_in ps_out) =
     do pp_in <- permPrettyM ps_in
        pp_out <- permPrettyM ps_out
-       return (pretty "lowned" <+> parens (align $
-                                           sep [pp_in, pretty "-o", pp_out]))
+       ls_pp <- case ls of
+         [] -> return emptyDoc
+         _ -> ppEncList False <$> mapM permPrettyM ls
+       return (pretty "lowned" <> ls_pp <+>
+               parens (align $ sep [pp_in, pretty "-o", pp_out]))
   permPrettyM (Perm_LCurrent l) = (pretty "lcurrent" <+>) <$> permPrettyM l
+  permPrettyM Perm_LFinished = return (pretty "lfinished")
   permPrettyM (Perm_Struct ps) =
     ((pretty "struct" <+>) . parens) <$> permPrettyM ps
   permPrettyM (Perm_Fun fun_perm) = permPrettyM fun_perm
@@ -2916,8 +2929,9 @@ isLLVMBlockPerm _ = False
 
 -- | Test if an 'AtomicPerm' is a lifetime permission
 isLifetimePerm :: AtomicPerm a -> Maybe (a :~: LifetimeType)
-isLifetimePerm (Perm_LOwned _ _) = Just Refl
+isLifetimePerm (Perm_LOwned _ _ _) = Just Refl
 isLifetimePerm (Perm_LCurrent _) = Just Refl
+isLifetimePerm Perm_LFinished = Just Refl
 isLifetimePerm _ = Nothing
 
 -- | Test if an 'AtomicPerm' is a struct permission
@@ -4410,8 +4424,9 @@ atomicPermIsCopyable (Perm_LLVMFunPtr _ _) = True
 atomicPermIsCopyable Perm_IsLLVMPtr = True
 atomicPermIsCopyable (Perm_LLVMBlockShape sh) = shapeIsCopyable PExpr_Write sh
 atomicPermIsCopyable (Perm_LLVMFrame _) = False
-atomicPermIsCopyable (Perm_LOwned _ _) = False
+atomicPermIsCopyable (Perm_LOwned _ _ _) = False
 atomicPermIsCopyable (Perm_LCurrent _) = True
+atomicPermIsCopyable Perm_LFinished = True
 atomicPermIsCopyable (Perm_Struct ps) = and $ RL.mapToList permIsCopyable ps
 atomicPermIsCopyable (Perm_Fun _) = True
 atomicPermIsCopyable (Perm_BVProp _) = True
@@ -4491,10 +4506,6 @@ lownedPermCouldProve (LOwnedPermBlock (PExpr_Var x) bp) ps =
                bvRangesCouldOverlap (llvmBlockRange bp) rng
              _ -> False) $
   varAtomicPermsInDistPerms x ps
-lownedPermCouldProve (LOwnedPermLifetime (PExpr_Var l) _ ps_out) ps =
-  any (\case Perm_LOwned _ _ -> True
-             _ -> False) (varAtomicPermsInDistPerms l ps) ||
-  lownedPermsCouldProve ps_out ps
 lownedPermCouldProve _ _ = False
 
 -- | Test if an 'LOwnedPerms' list could help prove any of a list of permissions
@@ -4657,9 +4668,10 @@ instance FreeVars (AtomicPerm tp) where
   freeVars Perm_IsLLVMPtr = NameSet.empty
   freeVars (Perm_LLVMBlockShape sh) = freeVars sh
   freeVars (Perm_LLVMFrame fperms) = freeVars $ map fst fperms
-  freeVars (Perm_LOwned ps_in ps_out) =
-    NameSet.union (freeVars ps_in) (freeVars ps_out)
+  freeVars (Perm_LOwned ls ps_in ps_out) =
+    NameSet.unions [freeVars ls, freeVars ps_in, freeVars ps_out]
   freeVars (Perm_LCurrent l) = freeVars l
+  freeVars Perm_LFinished = NameSet.empty
   freeVars (Perm_Struct ps) = NameSet.unions $ RL.mapToList freeVars ps
   freeVars (Perm_Fun fun_perm) = freeVars fun_perm
   freeVars (Perm_BVProp prop) = freeVars prop
@@ -4716,8 +4728,6 @@ instance FreeVars (LOwnedPerm a) where
     NameSet.unions [freeVars e, freeVars fp]
   freeVars (LOwnedPermBlock e bp) =
     NameSet.unions [freeVars e, freeVars bp]
-  freeVars (LOwnedPermLifetime e ps_in ps_out) =
-    NameSet.unions [freeVars e, freeVars ps_in, freeVars ps_out]
 
 instance FreeVars (LOwnedPerms ps) where
   freeVars = NameSet.unions . RL.mapToList freeVars
@@ -4780,7 +4790,7 @@ instance NeededVars (AtomicPerm a) where
   neededVars (Perm_LLVMArray ap) = neededVars ap
   neededVars (Perm_LLVMBlock bp) = neededVars bp
   neededVars (Perm_LLVMBlockShape _) = NameSet.empty
-  neededVars p@(Perm_LOwned _ _) = freeVars p
+  neededVars p@(Perm_LOwned _ _ _) = freeVars p
   neededVars p = freeVars p
 
 instance NeededVars (LLVMFieldPerm w sz) where
@@ -5043,9 +5053,10 @@ instance SubstVar s m => Substable s (AtomicPerm a) m where
     [nuMP| Perm_LLVMBlockShape sh |] ->
       Perm_LLVMBlockShape <$> genSubst s sh
     [nuMP| Perm_LLVMFrame fp |] -> Perm_LLVMFrame <$> genSubst s fp
-    [nuMP| Perm_LOwned ps_in ps_out |] ->
-      Perm_LOwned <$> genSubst s ps_in <*> genSubst s ps_out
+    [nuMP| Perm_LOwned ls ps_in ps_out |] ->
+      Perm_LOwned <$> genSubst s ls <*> genSubst s ps_in <*> genSubst s ps_out
     [nuMP| Perm_LCurrent e |] -> Perm_LCurrent <$> genSubst s e
+    [nuMP| Perm_LFinished |] -> return Perm_LFinished
     [nuMP| Perm_Struct tps |] -> Perm_Struct <$> genSubst s tps
     [nuMP| Perm_Fun fperm |] -> Perm_Fun <$> genSubst s fperm
     [nuMP| Perm_BVProp prop |] -> Perm_BVProp <$> genSubst s prop
@@ -5169,9 +5180,6 @@ instance SubstVar s m => Substable s (LOwnedPerm a) m where
       LOwnedPermField <$> genSubst s e <*> genSubst s fp
     [nuMP| LOwnedPermBlock e bp |] ->
       LOwnedPermBlock <$> genSubst s e <*> genSubst s bp
-    [nuMP| LOwnedPermLifetime e ps_in ps_out |] ->
-      LOwnedPermLifetime <$> genSubst s e <*> genSubst s ps_in
-                         <*> genSubst s ps_out
 
 instance SubstVar s m => Substable1 s LOwnedPerm m where
   genSubst1 = genSubst
@@ -5190,9 +5198,9 @@ instance SubstVar PermVarSubst m =>
          Substable PermVarSubst (LifetimeCurrentPerms ps) m where
   genSubst s mb_x = case mbMatch mb_x of
     [nuMP| AlwaysCurrentPerms |] -> return AlwaysCurrentPerms
-    [nuMP| LOwnedCurrentPerms l ps_in ps_out |] ->
-      LOwnedCurrentPerms <$> genSubst s l <*> genSubst s ps_in
-                         <*> genSubst s ps_out
+    [nuMP| LOwnedCurrentPerms l ls ps_in ps_out |] ->
+      LOwnedCurrentPerms <$> genSubst s l <*> genSubst s ls
+      <*> genSubst s ps_in <*> genSubst s ps_out
     [nuMP| CurrentTransPerms ps l |] ->
       CurrentTransPerms <$> genSubst s ps <*> genSubst s l
 
@@ -5794,13 +5802,16 @@ instance AbstractVars (AtomicPerm a) where
   abstractPEVars ns1 ns2 (Perm_LLVMFrame fp) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LLVMFrame |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 fp
-  abstractPEVars ns1 ns2 (Perm_LOwned ps_in ps_out) =
+  abstractPEVars ns1 ns2 (Perm_LOwned ls ps_in ps_out) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LOwned |])
+    `clMbMbApplyM` abstractPEVars ns1 ns2 ls
     `clMbMbApplyM` abstractPEVars ns1 ns2 ps_in
     `clMbMbApplyM` abstractPEVars ns1 ns2 ps_out
   abstractPEVars ns1 ns2 (Perm_LCurrent e) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LCurrent |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 e
+  abstractPEVars ns1 ns2 Perm_LFinished =
+    absVarsReturnH ns1 ns2 $(mkClosed [| Perm_LFinished |])
   abstractPEVars ns1 ns2 (Perm_Struct ps) =
     absVarsReturnH ns1 ns2 $(mkClosed [| Perm_Struct |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 ps
@@ -5930,11 +5941,6 @@ instance AbstractVars (LOwnedPerm a) where
     absVarsReturnH ns1 ns2 $(mkClosed [| LOwnedPermBlock |])
     `clMbMbApplyM` abstractPEVars ns1 ns2 e
     `clMbMbApplyM` abstractPEVars ns1 ns2 bp
-  abstractPEVars ns1 ns2 (LOwnedPermLifetime e ps_in ps_out) =
-    absVarsReturnH ns1 ns2 $(mkClosed [| LOwnedPermLifetime |])
-    `clMbMbApplyM` abstractPEVars ns1 ns2 e
-    `clMbMbApplyM` abstractPEVars ns1 ns2 ps_in
-    `clMbMbApplyM` abstractPEVars ns1 ns2 ps_out
 
 instance AbstractVars (LOwnedPerms ps) where
   abstractPEVars ns1 ns2 MNil =
@@ -6105,9 +6111,11 @@ instance AbstractNamedShape w (AtomicPerm a) where
   abstractNSM (Perm_NamedConj n args off) = 
     mbMap2 (Perm_NamedConj n) <$> abstractNSM args <*> abstractNSM off
   abstractNSM (Perm_LLVMFrame fp) = fmap Perm_LLVMFrame <$> abstractNSM fp
-  abstractNSM (Perm_LOwned ps_in ps_out) =
-    mbMap2 Perm_LOwned <$> abstractNSM ps_in <*> abstractNSM ps_out
+  abstractNSM (Perm_LOwned ls ps_in ps_out) =
+    mbMap3 Perm_LOwned <$> abstractNSM ls <*> abstractNSM ps_in <*>
+    abstractNSM ps_out
   abstractNSM (Perm_LCurrent e) = fmap Perm_LCurrent <$> abstractNSM e
+  abstractNSM Perm_LFinished = pureBindingM Perm_LFinished
   abstractNSM (Perm_Struct ps) = fmap Perm_Struct <$> abstractNSM ps
   abstractNSM (Perm_Fun fp) = fmap Perm_Fun <$> abstractNSM fp
   abstractNSM (Perm_BVProp prop) = pureBindingM (Perm_BVProp prop)
@@ -6146,9 +6154,6 @@ instance AbstractNamedShape w (LOwnedPerm a) where
     mbMap2 LOwnedPermField <$> abstractNSM e <*> abstractNSM fp
   abstractNSM (LOwnedPermBlock e bp) =
     mbMap2 LOwnedPermBlock <$> abstractNSM e <*> abstractNSM bp
-  abstractNSM (LOwnedPermLifetime e ps_in ps_out) =
-    mbMap3 LOwnedPermLifetime <$> abstractNSM e <*> abstractNSM ps_in
-                              <*> abstractNSM ps_out
 
 instance AbstractNamedShape w (ValuePerms as) where
   abstractNSM ValPerms_Nil = pureBindingM ValPerms_Nil
@@ -6637,7 +6642,7 @@ instance GetDetVarsClauses (AtomicPerm a) where
   getDetVarsClauses (Perm_LLVMBlockShape sh) = getDetVarsClauses sh
   getDetVarsClauses (Perm_LLVMFrame frame_perm) =
     concat <$> mapM (getDetVarsClauses . fst) frame_perm
-  getDetVarsClauses (Perm_LOwned _ _) = return []
+  getDetVarsClauses (Perm_LOwned _ _ _) = return []
   getDetVarsClauses _ = return []
 
 instance (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
index bee75fa0ca..fbd151329a 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs
@@ -990,8 +990,6 @@ abstractMbLOPsModalities mb_lops = case mbMatch mb_lops of
                LOwnedPermBlock e (bp { llvmBlockRW = PExpr_Var rw,
                                        llvmBlockLifetime = PExpr_Var l }))
       mb_e mb_bp)
-  [nuMP| lops :>: lop@(LOwnedPermLifetime _ _ _) |] ->
-    liftA2 (mbMap2 (:>:)) (abstractMbLOPsModalities lops) (pure lop)
 
 
 -- | Find all field or block permissions containing lifetime @l@ and return them
@@ -1058,11 +1056,11 @@ mbLifetimeFunPerm (LifetimeDef _ _ [] _)
          Some3FunPerm $ FunPerm (appendCruCtx
                                  (singletonCruCtx LifetimeRepr) ghosts) args ret
          (mbMap3 (\ps_in lops_in lops_in_abs ->
-                   assocAppend (MNil :>: ValPerm_LOwned lops_in lops_in_abs)
+                   assocAppend (MNil :>: ValPerm_LOwned [] lops_in lops_in_abs)
                    ghosts args_prxs $ distPermsToValuePerms ps_in)
           mb_ps_in mb_lops_in mb_lops_in_abs)
          (mbMap3 (\ps_out lops_out lops_in_abs ->
-                   assocAppend (MNil :>: ValPerm_LOwned lops_out lops_in_abs)
+                   assocAppend (MNil :>: ValPerm_LOwned [] lops_out lops_in_abs)
                    ghosts (args_prxs :>: Proxy) $ distPermsToValuePerms ps_out)
           mb_ps_out mb_lops_out (extMb mb_lops_in_abs))
 mbLifetimeFunPerm (LifetimeDef _ _ _bounds _) _ =
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 9da457a795..5a3ffad2cb 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -937,7 +937,8 @@ data AtomicPermTrans ctx a where
 
   -- | LOwned permissions translate to a monadic function from (the translation
   -- of) the input permissions to the output permissions
-  APTrans_LOwned :: Mb ctx (LOwnedPerms ps_in) ->
+  APTrans_LOwned :: Mb ctx [PermExpr LifetimeType] ->
+                    Mb ctx (LOwnedPerms ps_in) ->
                     Mb ctx (LOwnedPerms ps_out) ->
                     OpenTerm -> AtomicPermTrans ctx LifetimeType
 
@@ -945,6 +946,9 @@ data AtomicPermTrans ctx a where
   APTrans_LCurrent :: Mb ctx (PermExpr LifetimeType) ->
                       AtomicPermTrans ctx LifetimeType
 
+  -- | LFinished permissions have no computational content
+  APTrans_LFinished :: AtomicPermTrans ctx LifetimeType
+
   -- | The translation of a struct permission is sequence of the translations of
   -- the permissions in the struct permission
   APTrans_Struct :: PermTransCtx ctx (CtxToRList args) ->
@@ -1101,8 +1105,9 @@ instance IsTermTrans (AtomicPermTrans ctx a) where
   transTerms (APTrans_NamedConj _ _ _ t) = [t]
   transTerms (APTrans_DefinedNamedConj _ _ _ ptrans) = transTerms ptrans
   transTerms (APTrans_LLVMFrame _) = []
-  transTerms (APTrans_LOwned _ _ t) = [t]
+  transTerms (APTrans_LOwned _ _ _ t) = [t]
   transTerms (APTrans_LCurrent _) = []
+  transTerms APTrans_LFinished = []
   transTerms (APTrans_Struct pctx) = transTerms pctx
   transTerms (APTrans_Fun _ t) = [t]
   transTerms (APTrans_BVProp prop) = transTerms prop
@@ -1156,9 +1161,10 @@ atomicPermTransPerm _ (APTrans_NamedConj npn args off _) =
 atomicPermTransPerm _ (APTrans_DefinedNamedConj npn args off _) =
   mbMap2 (Perm_NamedConj npn) args off
 atomicPermTransPerm _ (APTrans_LLVMFrame fp) = fmap Perm_LLVMFrame fp
-atomicPermTransPerm _ (APTrans_LOwned ps_in ps_out _) =
-  mbMap2 Perm_LOwned ps_in ps_out
+atomicPermTransPerm _ (APTrans_LOwned ls ps_in ps_out _) =
+  mbMap3 Perm_LOwned ls ps_in ps_out
 atomicPermTransPerm _ (APTrans_LCurrent l) = fmap Perm_LCurrent l
+atomicPermTransPerm prxs APTrans_LFinished = nus prxs $ const Perm_LFinished
 atomicPermTransPerm prxs (APTrans_Struct ps) =
   fmap Perm_Struct $ permTransCtxPerms prxs ps
 atomicPermTransPerm _ (APTrans_Fun fp _) = fmap Perm_Fun fp
@@ -1217,9 +1223,10 @@ instance ExtPermTrans AtomicPermTrans where
   extPermTrans (APTrans_DefinedNamedConj npn args off ptrans) =
     APTrans_DefinedNamedConj npn (extMb args) (extMb off) (extPermTrans ptrans)
   extPermTrans (APTrans_LLVMFrame fp) = APTrans_LLVMFrame $ extMb fp
-  extPermTrans (APTrans_LOwned ps_in ps_out t) =
-    APTrans_LOwned (extMb ps_in) (extMb ps_out) t
+  extPermTrans (APTrans_LOwned ls ps_in ps_out t) =
+    APTrans_LOwned (extMb ls) (extMb ps_in) (extMb ps_out) t
   extPermTrans (APTrans_LCurrent p) = APTrans_LCurrent $ extMb p
+  extPermTrans APTrans_LFinished = APTrans_LFinished
   extPermTrans (APTrans_Struct ps) = APTrans_Struct $ RL.map extPermTrans ps
   extPermTrans (APTrans_Fun fp t) = APTrans_Fun (extMb fp) t
   extPermTrans (APTrans_BVProp prop_trans) =
@@ -1629,15 +1636,17 @@ instance TransInfo info =>
                          APTrans_NamedConj (mbLift npn) args off t) ptrans
     [nuMP| Perm_LLVMFrame fp |] ->
       return $ mkTypeTrans0 $ APTrans_LLVMFrame fp
-    [nuMP| Perm_LOwned ps_in ps_out |] ->
+    [nuMP| Perm_LOwned ls ps_in ps_out |] ->
       do tp_in <- translate1 ps_in
          tp_out <- translate1 ps_out
          let tp = arrowOpenTerm "ps" tp_in (applyOpenTerm
                                             (globalOpenTerm "Prelude.CompM")
                                             tp_out)
-         return $ mkTypeTrans1 tp (APTrans_LOwned ps_in ps_out)
+         return $ mkTypeTrans1 tp (APTrans_LOwned ls ps_in ps_out)
     [nuMP| Perm_LCurrent l |] ->
       return $ mkTypeTrans0 $ APTrans_LCurrent l
+    [nuMP| Perm_LFinished |] ->
+      return $ mkTypeTrans0 APTrans_LFinished
     [nuMP| Perm_Struct ps |] ->
       fmap APTrans_Struct <$> translate ps
     [nuMP| Perm_Fun fun_perm |] ->
@@ -2059,15 +2068,15 @@ translateSimplImpl :: Proxy ps -> Mb ctx (SimplImpl ps_in ps_out) ->
 translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
   [nuMP| SImpl_Drop _ _ |] ->
     withPermStackM (\(xs :>: _) -> xs) (\(ps :>: _) -> ps) m
-  
+
   [nuMP| SImpl_Copy x _ |] ->
     withPermStackM (:>: translateVar x) (\(ps :>: p) -> ps :>: p :>: p) m
-  
+
   [nuMP| SImpl_Swap _ _ _ _ |] ->
     withPermStackM (\(xs :>: x :>: y) -> xs :>: y :>: x)
     (\(pctx :>: px :>: py) -> pctx :>: py :>: px)
     m
-  
+
   [nuMP| SImpl_MoveUp (mb_ps1 :: DistPerms ps1) (_mb_x :: ExprVar a) _
                       (mb_ps2 :: DistPerms ps2) |] ->
     let ps1 = mbRAssignProxies mb_ps1
@@ -2087,7 +2096,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
               (pctx1, pctx2) = RL.split ps1 ps2 pctx12 in
           RL.append pctx0 $ RL.append (pctx1 :>: ptrans) pctx2)
         m
-  
+
   [nuMP| SImpl_MoveDown mb_ps1 (mb_x :: ExprVar a) _ mb_ps2 |]
     | prx_a <- mbLift $ fmap (const (Proxy :: Proxy a)) mb_x
     , ps1 <- mbRAssignProxies mb_ps1
@@ -2112,7 +2121,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          (\(ps :>: p_top) ->
            ps :>: PTrans_Term (mbMap2 ValPerm_Or p1 p2) (leftTrans tp1 tp2 p_top))
          m
-  
+
   [nuMP| SImpl_IntroOrR _ p1 p2 |] ->
     do tp1 <- translate p1
        tp2 <- translate p2
@@ -2120,7 +2129,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          (\(ps :>: p_top) ->
            ps :>: PTrans_Term (mbMap2 ValPerm_Or p1 p2) (rightTrans tp1 tp2 p_top))
          m
-  
+
   [nuMP| SImpl_IntroExists _ e p |] ->
     do let tp = mbExprType e
        tp_trans <- translateClosed tp
@@ -2131,12 +2140,12 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        withPermStackM id
          ((:>: PTrans_Term (fmap ValPerm_Exists p) sigma_trm) . RL.tail)
          m
-  
+
   [nuMP| SImpl_Cast _ _ _ |] ->
     withPermStackM RL.tail
     (\(pctx :>: _ :>: ptrans) -> pctx :>: ptrans)
     m
-  
+
   [nuMP| SImpl_CastPerm (x::ExprVar a) eqp |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        let prxs_a = MNil :>: (Proxy :: Proxy a)
@@ -2149,34 +2158,34 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                (_ :>: ptrans, _) = RL.split prxs_a prxs1 pctx2 in
            pctx1 :>: typeTransF ttrans (transTerms ptrans))
          m
-  
+
   [nuMP| SImpl_IntroEqRefl x |] ->
     withPermStackM (:>: translateVar x) (:>: PTrans_Eq (fmap PExpr_Var x)) m
-  
+
   [nuMP| SImpl_InvertEq x y |] ->
     withPermStackM ((:>: translateVar y) . RL.tail)
     ((:>: PTrans_Eq (fmap PExpr_Var x)) . RL.tail)
     m
-  
+
   [nuMP| SImpl_InvTransEq _ mb_y _ |] ->
     withPermStackM RL.tail
     ((:>: PTrans_Eq (fmap PExpr_Var mb_y)) . RL.tail . RL.tail)
     m
-  
+
   [nuMP| SImpl_CopyEq _ _ |] ->
     withPermStackM
     (\(vars :>: var) -> (vars :>: var :>: var))
     (\(pctx :>: ptrans) -> (pctx :>: ptrans :>: ptrans))
     m
-  
+
   [nuMP| SImpl_LLVMWordEq _ _ e |] ->
     withPermStackM RL.tail
     (\(pctx :>: _ :>: _) -> (pctx :>: PTrans_Eq (fmap PExpr_LLVMWord e)))
     m
-  
+
   [nuMP| SImpl_IntroConj x |] ->
     withPermStackM (:>: translateVar x) (:>: PTrans_True) m
-  
+
   [nuMP| SImpl_ExtractConj x _ mb_i |] ->
     withPermStackM (:>: translateVar x)
     (\(pctx :>: ptrans) ->
@@ -2188,7 +2197,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
       else
         error "translateSimplImpl: SImpl_ExtractConj: index out of bounds")
     m
-  
+
   [nuMP| SImpl_CopyConj x _ mb_i |] ->
     withPermStackM (:>: translateVar x)
     (\(pctx :>: ptrans) ->
@@ -2197,7 +2206,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
       if i < length ps then pctx :>: PTrans_Conj [ps !! i] :>: ptrans else
         error "translateSimplImpl: SImpl_CopyConj: index out of bounds")
     m
-  
+
   [nuMP| SImpl_InsertConj _ _ _ i |] ->
     withPermStackM RL.tail
     (\(pctx :>: ptransi :>: ptrans) ->
@@ -2205,7 +2214,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
           pi = unPTransConj1 "translateSimplImpl: SImpl_InsertConj" ptransi in
       pctx :>: PTrans_Conj (take (mbLift i) ps ++ pi : drop (mbLift i) ps))
     m
-  
+
   [nuMP| SImpl_AppendConjs _ _ _ |] ->
     withPermStackM RL.tail
     (\(pctx :>: ptrans1 :>: ptrans2) ->
@@ -2213,7 +2222,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
           ps2 = unPTransConj "translateSimplImpl: SImpl_AppendConjs" ptrans2 in
       pctx :>: PTrans_Conj (ps1 ++ ps2))
     m
-  
+
   [nuMP| SImpl_SplitConjs x _ mb_i |] ->
     let i = mbLift mb_i in
     withPermStackM (:>: translateVar x)
@@ -2221,13 +2230,13 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
       let ps = unPTransConj "translateSimplImpl: SImpl_SplitConjs" ptrans in
       pctx :>: PTrans_Conj (take i ps) :>: PTrans_Conj (drop i ps))
     m
-  
+
   [nuMP| SImpl_IntroStructTrue x prxs |] ->
     withPermStackM (:>: translateVar x)
     (\pctx -> pctx :>: PTrans_Conj [APTrans_Struct $
                                     RL.map (const PTrans_True) (mbRAssign prxs)])
     m
-  
+
   [nuMP| SImpl_StructEqToPerm _ exprs |] ->
     withPermStackM id
     (\(pctx :>: _) ->
@@ -2235,19 +2244,19 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                             RL.map (PTrans_Eq . getCompose)
                             (mbRAssign $ fmap exprsToRAssign exprs)])
     m
-  
+
   [nuMP| SImpl_StructPermToEq _ exprs |] ->
     withPermStackM id
     (\(pctx :>: _) -> pctx :>: PTrans_Eq (fmap PExpr_Struct exprs))
     m
-  
+
   [nuMP| SImpl_IntroStructField _ _ memb _ |] ->
     withPermStackM RL.tail
     (\(pctx :>: PTrans_Conj [APTrans_Struct pctx_str] :>: ptrans) ->
       pctx :>: PTrans_Conj [APTrans_Struct $
                             RL.set (mbLift memb) ptrans pctx_str])
     m
-  
+
   [nuMP| SImpl_ConstFunPerm x _ mb_fun_perm ident |] ->
     withPermStackM ((:>: translateVar x) . RL.tail)
     ((:>: PTrans_Term (fmap (ValPerm_Conj1
@@ -2255,37 +2264,37 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                                                        mbLift ident))
      . RL.tail)
     m
-  
+
   [nuMP| SImpl_CastLLVMWord _ _ e2 |] ->
     withPermStackM RL.tail
     ((:>: PTrans_Eq (fmap PExpr_LLVMWord e2)) . RL.tail . RL.tail)
     m
-  
+
   [nuMP| SImpl_InvertLLVMOffsetEq mb_x mb_off mb_y |] ->
     withPermStackM
     ((:>: translateVar mb_y) . RL.tail)
     ((:>: PTrans_Eq (mbMap2 (\x off -> PExpr_LLVMOffset x $
                                        bvNegate off) mb_x mb_off)) . RL.tail)
     m
-  
+
   [nuMP| SImpl_OffsetLLVMWord _ mb_e mb_off mb_x |] ->
     withPermStackM
     ((:>: translateVar mb_x) . RL.tail . RL.tail)
     ((:>: PTrans_Eq (mbMap2 (\e off -> PExpr_LLVMWord $ bvAdd e off)
                      mb_e mb_off)) . RL.tail . RL.tail)
     m
-  
+
   [nuMP| SImpl_CastLLVMPtr _ _ off _ |] ->
     withPermStackM RL.tail
     (\(pctx :>: _ :>: ptrans) ->
       pctx :>: offsetLLVMPermTrans (fmap bvNegate off) ptrans)
     m
-  
+
   [nuMP| SImpl_CastLLVMFree _ _ e2 |] ->
     withPermStackM RL.tail
     ((:>: PTrans_Conj [APTrans_LLVMFree e2]) . RL.tail . RL.tail)
     m
-  
+
   [nuMP| SImpl_CastLLVMFieldOffset _ mb_fld mb_off |] ->
     withPermStackM RL.tail
     (\(pctx :>: _ :>: ptrans) ->
@@ -2297,13 +2306,13 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                              mb_fld mb_off)
                             ptrans'])
     m
-  
+
   [nuMP| SImpl_IntroLLVMFieldContents x _ mb_fld |] ->
     withPermStackM ((:>: translateVar x) . RL.tail . RL.tail)
     (\(pctx :>: _ :>: ptrans) ->
       pctx :>: PTrans_Conj [APTrans_LLVMField mb_fld ptrans])
     m
-  
+
   [nuMP| SImpl_DemoteLLVMFieldRW _ mb_fld |] ->
     withPermStackM id
     (\(pctx :>: ptrans) ->
@@ -2315,7 +2324,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                             (fmap (\fld -> fld { llvmFieldRW = PExpr_Read }) mb_fld)
                             ptrans'])
     m
-  
+
   [nuMP| SImpl_LLVMArrayCopy _ mb_ap mb_sub_ap |] ->
     do let _w = natVal2 mb_ap
        sub_ap_tp_trans <- translate mb_sub_ap
@@ -2335,7 +2344,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                         rng_trans {- mb_sub_borrows -} prop_transs]
            :>: ptrans_array)
          m
-  
+
   [nuMP| SImpl_LLVMArrayBorrow _ mb_ap mb_sub_ap |] ->
     do sub_ap_tp_trans <- translate mb_sub_ap
        let mb_rng = mbMap2 llvmSubArrayRange mb_ap mb_sub_ap
@@ -2366,7 +2375,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            PTrans_Conj [sub_array_trans]
            :>: PTrans_Conj [APTrans_LLVMArray array_trans'])
          m
-  
+
   [nuMP| SImpl_LLVMArrayReturn _ mb_ap mb_ret_ap |] ->
     do (_ :>: ptrans_sub_array :>: ptrans_array) <- itiPermStack <$> ask
        let mb_cell =
@@ -2392,7 +2401,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          (\(pctx :>: _ :>: _) ->
            pctx :>: PTrans_Conj [APTrans_LLVMArray array_trans'])
          m
-  
+
   [nuMP| SImpl_LLVMArrayAppend _ mb_ap1 mb_ap2 |] ->
     withPermStackM RL.tail
     (\(pctx :>: ptrans_array1 :>: ptrans_array2) ->
@@ -2422,8 +2431,8 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                 llvmArrayTransTerm array_trans2] } in
        pctx :>: PTrans_Conj [APTrans_LLVMArray array_trans_out])
     m
-  
-  
+
+
   [nuMP| SImpl_LLVMArrayRearrange _ _ mb_ap2 |] ->
     do ap2_tp_trans <- translate mb_ap2
        withPermStackM id
@@ -2432,13 +2441,13 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            PTrans_Conj [APTrans_LLVMArray $
                         typeTransF ap2_tp_trans [transTerm1 ptrans_array]])
          m
-  
+
   [nuMP| SImpl_LLVMArrayToField _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: _) -> pctx :>: typeTransF ttrans [])
          m
-  
+
   [nuMP| SImpl_LLVMArrayEmpty x mb_ap |] ->
     do (w_term, _, elem_tp, ap_tp_trans) <- translateLLVMArrayPerm mb_ap
        let arr_term =
@@ -2449,7 +2458,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            pctx :>:
            PTrans_Conj [APTrans_LLVMArray $ typeTransF ap_tp_trans [arr_term]])
          m
-  
+
   [nuMP| SImpl_LLVMArrayOneCell _ mb_ap |] ->
     do (w_term, len_term, elem_tp, ap_tp_trans) <- translateLLVMArrayPerm mb_ap
        withPermStackM id
@@ -2460,8 +2469,8 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            pctx :>:
            PTrans_Conj [APTrans_LLVMArray $ typeTransF ap_tp_trans [arr_term]])
          m
-  
-  
+
+
   [nuMP| SImpl_LLVMArrayIndexCopy _ _ mb_ix |] ->
     do (_ :>: ptrans_array :>: ptrans_props) <- itiPermStack <$> ask
        let arr_trans =
@@ -2476,7 +2485,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          (\(pctx :>: _ :>: _) ->
            pctx :>: PTrans_Conj [fld_ptrans] :>: ptrans_array)
          m
-  
+
   [nuMP| SImpl_LLVMArrayIndexBorrow _ mb_ap mb_ix |] ->
     do (_ :>: ptrans_array :>: ptrans_props) <- itiPermStack <$> ask
        let arr_trans =
@@ -2498,7 +2507,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            pctx :>: PTrans_Conj [fld_ptrans] :>:
            PTrans_Conj [APTrans_LLVMArray arr_trans'])
          m
-  
+
   [nuMP| SImpl_LLVMArrayIndexReturn _ mb_ap mb_ix |] ->
     do (_ :>: ptrans_fld :>: ptrans_array) <- itiPermStack <$> ask
        let aptrans_fld = case ptrans_fld of
@@ -2520,29 +2529,29 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          (\(pctx :>: _ :>: _) ->
            pctx :>: PTrans_Conj [APTrans_LLVMArray arr_trans'])
          m
-  
+
   [nuMP| SImpl_LLVMArrayContents _ _ _ _ _ |] ->
     error "FIXME HERE: translateSimplImpl: SImpl_LLVMArrayContents unhandled"
-  
+
   [nuMP| SImpl_LLVMFieldIsPtr x _ |] ->
     withPermStackM (:>: translateVar x)
     (\(pctx :>: ptrans_fld) ->
       pctx :>: PTrans_Conj [APTrans_IsLLVMPtr] :>: ptrans_fld)
     m
-  
+
   [nuMP| SImpl_LLVMArrayIsPtr x _ |] ->
     withPermStackM (:>: translateVar x)
     (\(pctx :>: ptrans_array) ->
       pctx :>: PTrans_Conj [APTrans_IsLLVMPtr] :>: ptrans_array)
     m
-  
+
   [nuMP| SImpl_LLVMBlockIsPtr x _ |] ->
     withPermStackM (:>: translateVar x)
     (\(pctx :>: ptrans) ->
       pctx :>: PTrans_Conj [APTrans_IsLLVMPtr] :>: ptrans)
     m
-  
-  [nuMP| SImpl_SplitLifetime _ f args l _ ps_in ps_out |] ->
+
+  [nuMP| SImpl_SplitLifetime _ f args l _ _ ps_in ps_out |] ->
     do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
        ps_in_tp <- translate1 ps_in
        ps_out_tp <- translate1 ps_out
@@ -2565,30 +2574,36 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            RL.append pctx $
            typeTransF pctx_out_trans (transTerms ptrans_x ++ [f_tm]))
          m
-  
-  [nuMP| SImpl_SubsumeLifetime _ _ ps_in1 ps_out1 ps_in2 ps_out2 |] ->
+
+  [nuMP| SImpl_SubsumeLifetime _ _ _ _ _ |] ->
     do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
-       ps_in1_tp <- translate1 ps_in1
-       ps_out1_tp <- translate1 ps_out1
-       ps_in2_tp <- translate1 ps_in2
-       ps_out2_tp <- translate1 ps_out2
-       let fun_tp1 = arrowOpenTerm "ps" ps_in1_tp (applyOpenTerm
-                                                   (globalOpenTerm "Prelude.CompM")
-                                                   ps_out1_tp)
        withPermStackM id
-         (\(pctx :>: ptrans_l1 :>: ptrans_l2) ->
-           -- The output permissions are an lcurrent permission, which has no term
-           -- translation, and the updated lowned permission, which is the result
-           -- of adding the translation of the lowned permission for l1 to the
-           -- return value of that for l2
-           RL.append pctx $
-           typeTransF pctx_out_trans [applyOpenTermMulti
-                                      (globalOpenTerm "Prelude.tupleCompMFunOut")
-                                      [ps_in2_tp, ps_out2_tp, fun_tp1,
-                                       transTerm1 ptrans_l1,
-                                       transTerm1 ptrans_l2]])
+         (\(pctx :>: ptrans_l) ->
+           RL.append pctx $ typeTransF pctx_out_trans (transTerms ptrans_l))
+         m
+
+  [nuMP| SImpl_ContainedLifetimeCurrent _ _ _ _ _ |] ->
+    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+       withPermStackM
+         (\(ns :>: l1) -> ns :>: l1 :>: l1)
+         (\(pctx :>: ptrans_l) ->
+           -- Note: lcurrent perms do not contain any terms and the term for the
+           -- lowned permission does not change, so the only terms in both the
+           -- input and the output are in ptrans_l
+           RL.append pctx $ typeTransF pctx_out_trans (transTerms ptrans_l))
          m
-  
+
+  [nuMP| SImpl_RemoveContainedLifetime _ _ _ _ _ |] ->
+    do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
+       withPermStackM
+         (\(ns :>: l1 :>: _) -> ns :>: l1)
+         (\(pctx :>: ptrans_l :>: _) ->
+           -- Note: lcurrent perms do not contain any terms and the term for the
+           -- lowned permission does not change, so the only terms in both the
+           -- input and the output are in ptrans_l
+           RL.append pctx $ typeTransF pctx_out_trans (transTerms ptrans_l))
+         m
+
   [nuMP| SImpl_WeakenLifetime _ _ _ _ _ |] ->
     do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
        withPermStackM RL.tail
@@ -2598,9 +2613,9 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            -- ptrans_x to pctx_out_trans
            RL.append pctx (typeTransF pctx_out_trans $ transTerms ptrans_x))
          m
-  
-  [nuMP| SImpl_MapLifetime l ps_in ps_out
-                                  ps_in' ps_out' ps1 ps2 impl_in impl_out |] ->
+
+  [nuMP| SImpl_MapLifetime l _ ps_in ps_out
+                           ps_in' ps_out' ps1 ps2 impl_in impl_out |] ->
     -- First, translate the output permissions and all of the perm lists
     do pctx_out_trans <- translate $ fmap simplImplOut mb_simpl
        ps_in_trans <- translate ps_in
@@ -2609,7 +2624,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        ps_out'_trans <- translate ps_out'
        -- ps1_trans <- translate ps1
        -- ps2_trans <- translate ps2
-  
+
        -- Next, split out the various input permissions from the rest of the pctx
        let prxs1 = mbRAssignProxies ps1
        let prxs2 = mbRAssignProxies ps2
@@ -2617,13 +2632,13 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        pctx <- itiPermStack <$> ask
        let (pctx_ps, pctx12 :>: ptrans_l) = RL.split ps0 prxs_in pctx
        let (pctx1, pctx2) = RL.split prxs1 prxs2 pctx12
-  
+
        -- Also split out the input variables and replace them with the ps_out vars
        pctx_vars <- itiPermStackVars <$> ask
        let (vars_ps, vars12 :>: _) = RL.split ps0 prxs_in pctx_vars
        let (vars1, vars2) = RL.split prxs1 prxs2 vars12
        let vars_out = vars_ps :>: translateVar l
-  
+
        -- Now build the output lowned function by composing the input lowned
        -- function with the translations of the implications on inputs and outputs
        let fromJustOrError (Just x) = x
@@ -2649,23 +2664,23 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
               (globalOpenTerm "Prelude.composeM")
               [transTerm1 ps_in_trans, transTerm1 ps_out_trans,
                transTerm1 ps_out'_trans, transTerm1 ptrans_l, impl_out_tm]]
-  
+
        -- Finally, update the permissions
        withPermStackM
          (\_ -> vars_out)
          (\_ -> RL.append pctx_ps $ typeTransF pctx_out_trans [l_res_tm])
          m
-  
+
   [nuMP| SImpl_EndLifetime _ ps_in ps_out |] ->
     -- First, translate the output permissions and the input and output types of
     -- the monadic function for the lifeime ownership permission
     do ps_out_trans <- translate ps_out
        let prxs_in = mbRAssignProxies ps_in :>: Proxy
-  
+
        -- Next, split out the ps_in permissions from the rest of the pctx
        pctx <- itiPermStack <$> ask
        let (pctx_ps, pctx_in :>: ptrans_l) = RL.split ps0 prxs_in pctx
-  
+
        -- Also split out the ps_in variables and replace them with the ps_out vars
        pctx_vars <- itiPermStackVars <$> ask
        let (ps_vars, _ :>: _) = RL.split ps0 prxs_in pctx_vars
@@ -2674,7 +2689,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        let vars_out =
              RL.append ps_vars $ RL.map (translateVar . getCompose) $
              mbRAssign $ fmap (fromJustHelper . lownedPermsVars) ps_out
-  
+
        -- Now we apply the lifetime ownerhip function to ps_in and bind its output
        -- in the rest of the computation
        applyMultiTransM (return $ globalOpenTerm "Prelude.bindM")
@@ -2683,39 +2698,40 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                   (strictTransTupleTerm pctx_in)),
           lambdaTransM "endl_ps" ps_out_trans $ \pctx_out ->
            withPermStackM
-           (\_ -> vars_out)
-           (\_ -> RL.append pctx_ps pctx_out)
+           (\(_ :>: l) -> vars_out :>: l)
+           (\_ -> RL.append pctx_ps pctx_out :>:
+                  PTrans_Conj [APTrans_LFinished])
            m]
-  
+
   [nuMP| SImpl_LCurrentRefl l |] ->
     withPermStackM (:>: translateVar l)
     (:>: PTrans_Conj [APTrans_LCurrent $ fmap PExpr_Var l])
     m
-  
+
   [nuMP| SImpl_LCurrentTrans _l1 _l2 l3 |] ->
     withPermStackM RL.tail
     ((:>: PTrans_Conj [APTrans_LCurrent l3]) .
      RL.tail . RL.tail)
     m
-  
+
   [nuMP| SImpl_DemoteLLVMBlockRW _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans (transTerms ptrans))
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockEmpty x _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM (:>: translateVar x)
          (\pctx -> pctx :>: typeTransF ttrans [unitOpenTerm])
          m
-  
+
   [nuMP| SImpl_CoerceLLVMBlockEmpty _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: _) -> pctx :>: typeTransF ttrans [unitOpenTerm])
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockToBytes _ mb_bp |] ->
     do let w = natVal2 mb_bp
        let w_term = natOpenTerm w
@@ -2728,7 +2744,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                  [w_term, len_term, unitTypeOpenTerm, unitOpenTerm] in
            pctx :>: typeTransF ttrans [arr_term])
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockSeqEmpty _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
@@ -2736,14 +2752,14 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            pctx :>: typeTransF ttrans [pairOpenTerm (transTerm1 ptrans)
                                        unitOpenTerm])
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockSeqEmpty _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [pairLeftOpenTerm (transTerm1 ptrans)])
          m
-  
+
   -- Intro for a recursive named shape applies the fold function to the
   -- translations of the arguments plus the translations of the proofs of the
   -- permissions
@@ -2803,35 +2819,35 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            m
 
     | otherwise -> fail "translateSimplImpl: ElimLLVMBlockNamed, unknown named shape"
-  
+
   [nuMP| SImpl_IntroLLVMBlockFromEq _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM RL.tail
          (\(pctx :>: _ :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockPtr _ _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans (transTerms ptrans))
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockPtr _ _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans (transTerms ptrans))
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockField _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTupleTerm ptrans])
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockField _ _ _ |] ->
     do let mb_ps = fmap ((\case ValPerm_Conj ps -> ps
                                 _ -> error "translateSimplImpl: SImpl_ElimLLVMBlockField, VPerm_Conj required"
@@ -2844,21 +2860,21 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            PTrans_Conj [typeTransF (tupleTypeTrans ttrans1) [transTerm1 ptrans],
                         typeTransF ttrans2 [unitOpenTerm]])
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockArray _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockArray _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockSeq _ _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM RL.tail
@@ -2867,7 +2883,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                  pairOpenTerm (transTerm1 ptrans1) (transTerm1 ptrans2) in
            pctx :>: typeTransF ttrans [pair_term])
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockSeq _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
@@ -2875,31 +2891,31 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            pctx :>: typeTransF ttrans [pairLeftOpenTerm (transTerm1 ptrans),
                                        pairRightOpenTerm (transTerm1 ptrans)])
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockOr _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockOr _ _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
-  
+
   [nuMP| SImpl_IntroLLVMBlockEx _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
-  
+
   [nuMP| SImpl_ElimLLVMBlockEx _ _ |] ->
     do ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) -> pctx :>: typeTransF ttrans [transTerm1 ptrans])
          m
-  
+
   [nuMP| SImpl_FoldNamed _ (NamedPerm_Rec rp) args _ |] ->
     do args_trans <- translate args
        ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
@@ -2911,7 +2927,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                                        (transTerms args_trans
                                         ++ transTerms ptrans_x)])
          m
-  
+
   [nuMP| SImpl_UnfoldNamed _ (NamedPerm_Rec rp) args _ |] ->
     do args_trans <- translate args
        ttrans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
@@ -2924,7 +2940,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
                                                (transTerms args_trans
                                                 ++ [transTerm1 ptrans_x])])
          m
-  
+
   [nuMP| SImpl_FoldNamed _ (NamedPerm_Defined dp) args off |] ->
     do folded_trans <-
          translate (mbMap2 ValPerm_Named (fmap definedPermName dp) args
@@ -2933,7 +2949,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF folded_trans (transTerms ptrans))
          m
-  
+
   [nuMP| SImpl_UnfoldNamed _ (NamedPerm_Defined dp) args off |] ->
     do unfolded_trans <-
          translate (mbMap2 unfoldDefinedPerm dp args `mbApply` off)
@@ -2941,48 +2957,48 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF unfolded_trans (transTerms ptrans))
          m
-  
+
   {-
   [nuMP| SImpl_Mu _ _ _ _ |] ->
     error "FIXME HERE: SImpl_Mu: translation not yet implemented"
   -}
-  
+
   [nuMP| SImpl_NamedToConj _ _ _ _ |] ->
     do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
-  
+
   [nuMP| SImpl_NamedFromConj _ _ _ _ |] ->
     do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
-  
+
   [nuMP| SImpl_NamedArgAlways _ _ _ _ _ _ |] ->
     do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
-  
+
   [nuMP| SImpl_NamedArgCurrent _ _ _ _ _ _ |] ->
     do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM RL.tail
          (\(pctx :>: ptrans :>: _) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
-  
+
   [nuMP| SImpl_NamedArgWrite _ _ _ _ _ _ |] ->
     do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
-  
+
   [nuMP| SImpl_NamedArgRead _ _ _ _ _ |] ->
     do tp_trans <- translate $ fmap (distPermsHeadPerm . simplImplOut) mb_simpl
        withPermStackM id
          (\(pctx :>: ptrans) ->
            pctx :>: typeTransF tp_trans (transTerms ptrans)) m
-  
+
   [nuMP| SImpl_ReachabilityTrans _ rp args _ y e |] ->
     do args_trans <- translate $ mbMap2 PExprs_Cons args e
        y_trans <- translate y
@@ -3081,7 +3097,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
   -- Impl1_Catch, if one exists, or the SAW errorM function otherwise
   ([nuMP| Impl1_Fail str |], _) ->
     tell [mbLift str] >> mzero
-  
+
   ([nuMP| Impl1_Catch |],
    [nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) ->
     pitmCatching (translatePermImpl prx $ mbCombine RL.typeCtxProxies mb_impl1) >>= \maybe_trans1 ->
@@ -3094,7 +3110,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
         (\catchpoint -> trans1 $ ImplFailContTerm catchpoint)
       (Nothing, Just trans2) -> return trans2
       (_, Nothing) -> pitmMaybeRet maybe_trans1
-  
+
   -- A push moves the given permission from x to the top of the perm stack
   ([nuMP| Impl1_Push x p |], _) ->
     translatePermImplUnary mb_impls $ \m ->
@@ -3102,7 +3118,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
        ptrans <- getVarPermM x
        setVarPermM x (PTrans_True)
          (withPermStackM (:>: translateVar x) (:>: ptrans) m)
-  
+
   -- A pop moves the given permission from the top of the perm stack to x
   ([nuMP| Impl1_Pop x p |], _) ->
     translatePermImplUnary mb_impls $ \m ->
@@ -3111,7 +3127,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
                                              const ValPerm_True)
        ptrans <- getTopPermM
        setVarPermM x ptrans (withPermStackM RL.tail RL.tail m)
-  
+
   -- If both branches of an or elimination fail, the whole thing fails; otherwise,
   -- an or elimination performs a pattern-match on an Either
   ([nuMP| Impl1_ElimOr x p1 p2 |],
@@ -3135,7 +3151,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
                withPermStackM id ((:>: ptrans) . RL.tail) $
                forceImplTrans maybe_trans2 k)
              (transTupleTerm top_ptrans)
-  
+
   -- An existential elimination performs a pattern-match on a Sigma
   ([nuMP| Impl1_ElimExists x p |], _) ->
     translatePermImplUnary mb_impls $ \m ->
@@ -3150,7 +3166,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
            inExtTransM etrans $
            withPermStackM id ((:>: ptrans) . RL.tail) m)
          (transTerm1 top_ptrans)
-  
+
   -- A SimplImpl is translated using translateSimplImpl
   ([nuMP| Impl1_Simpl simpl mb_prx |], _) ->
     let prx' = mbLift mb_prx in
@@ -3159,14 +3175,14 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
     translateSimplImpl prx' simpl $
     do () <- assertPermStackTopEqM "SimplImpl out" prx' (fmap simplImplOut simpl)
        m
-  
+
   -- A let binding becomes a let binding
   ([nuMP| Impl1_LetBind _ e |], _) ->
     translatePermImplUnary mb_impls $ \m ->
     do etrans <- translate e
        inExtTransM etrans $
          withPermStackM (:>: Member_Base) (:>: PTrans_Eq (extMb e)) m
-  
+
   ([nuMP| Impl1_ElimStructField x _ _ memb |], _) ->
     translatePermImplUnary mb_impls $ \m ->
     do etrans_x <- translate x
@@ -3181,7 +3197,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
                                  RL.set (mbLift memb) (PTrans_Eq mb_y) pctx_str]
            :>: RL.get (mbLift memb) pctx_str)
          m
-  
+
   ([nuMP| Impl1_ElimLLVMFieldContents _ mb_fld |], _) ->
     translatePermImplUnary mb_impls $ \m ->
     inExtTransM ETrans_LLVM $
@@ -3200,7 +3216,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
                                        fmap (const $ nu PExpr_Var) mb_fld)]
       :>: ptrans')
     m
-  
+
   ([nuMP| Impl1_ElimLLVMBlockToEq _ mb_bp |], _) ->
     translatePermImplUnary mb_impls $ \m ->
     inExtTransM ETrans_LLVMBlock $
@@ -3218,17 +3234,17 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
            pctx :>: typeTransF tp_trans1 [unitOpenTerm] :>:
            typeTransF tp_trans2 [transTerm1 ptrans])
          m
-  
+
   ([nuMP| Impl1_BeginLifetime |], _) ->
     translatePermImplUnary mb_impls $ \m ->
     inExtTransM ETrans_Lifetime $
-    do tp_trans <- translateClosed $ ValPerm_LOwned MNil MNil
+    do tp_trans <- translateClosed $ ValPerm_LOwned [] MNil MNil
        let id_fun =
              lambdaOpenTerm "ps_empty" unitTypeOpenTerm $ \x ->
              applyOpenTermMulti (globalOpenTerm "Prelude.returnM")
              [unitTypeOpenTerm, x]
        withPermStackM (:>: Member_Base) (:>: typeTransF tp_trans [id_fun]) m
-  
+
   -- If e1 and e2 are already equal, short-circuit the proof construction and then
   -- elimination
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Eq e1 e2) _ |], _)
@@ -3240,12 +3256,12 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
          withPermStackM (:>: translateVar x)
            (:>: PTrans_Conj [APTrans_BVProp (BVPropTrans prop pf)])
            m
-  
+
   -- If e1 and e2 are definitely not equal, treat this as a fail
   ([nuMP| Impl1_TryProveBVProp _ (BVProp_Eq e1 e2) prop_str |], _)
     | not $ mbLift (mbMap2 bvCouldEqual e1 e2) ->
       tell [mbLift prop_str] >> mzero
-  
+
   -- Otherwise, insert an equality test with proof construction. Note that, as
   -- with all TryProveBVProps, if the test fails and there is no failure
   -- continuation, we insert just the proposition failure string using
@@ -3265,7 +3281,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
              trans k)
          , applyMultiTransM (return $ globalOpenTerm "Prelude.bvEqWithProof")
            [ return (natOpenTerm $ natVal2 prop) , translate1 e1, translate1 e2]]
-  
+
   -- For an inequality test, we don't need a proof, so just insert an if
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Neq e1 e2) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->
@@ -3280,7 +3296,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
     , withPermStackM (:>: translateVar x)
       (:>: PTrans_Conj [APTrans_BVProp (BVPropTrans prop unitOpenTerm)]) $
       trans k]
-  
+
   {-
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULt e1 e2) _ |],
    [nuMP| MbPermImpls_Cons _ mb_impl' |])
@@ -3291,7 +3307,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
                                                      globalOpenTerm "Prelude.True"])))
       (translate $ mbCombine mb_impl')
   -}
-  
+
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULt e1 e2) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->
     translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
@@ -3307,7 +3323,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
          , applyMultiTransM (return $ globalOpenTerm "Prelude.bvultWithProof")
            [ return (natOpenTerm $ natVal2 prop), translate1 e1, translate1 e2]
          ]
-  
+
   {-
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq e1 e2) _ |],
    [nuMP| MbPermImpls_Cons _ mb_impl' |])
@@ -3318,7 +3334,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
                                                      globalOpenTerm "Prelude.True"])))
       (translate $ mbCombine mb_impl')
   -}
-  
+
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq e1 e2) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->
     translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
@@ -3334,8 +3350,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
          , applyMultiTransM (return $ globalOpenTerm "Prelude.bvuleWithProof")
            [ return (natOpenTerm $ natVal2 prop), translate1 e1, translate1 e2]
          ]
-  
-  
+
+
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq_Diff e1 e2 e3) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->
     translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
@@ -3461,9 +3477,9 @@ instance (PermCheckExtC ext, TransInfo info) =>
       ETrans_Term <$>
       applyMultiTransM (return $ globalOpenTerm "Prelude.bvEq")
       [translate w, translateRWV e1, translateRWV e2]
-  
+
     [nuMP| EmptyApp |] -> return ETrans_Unit
-  
+
     -- Booleans
     [nuMP| BoolLit True |] ->
       return $ ETrans_Term $ globalOpenTerm "Prelude.True"
@@ -3485,7 +3501,7 @@ instance (PermCheckExtC ext, TransInfo info) =>
       ETrans_Term <$>
       applyMultiTransM (return $ globalOpenTerm "Prelude.xor")
       [translateRWV e1, translateRWV e2]
-  
+
     -- Natural numbers
     [nuMP| Expr.NatLit n |] ->
       return $ ETrans_Term $ natOpenTerm $ mbLift n
@@ -3518,11 +3534,11 @@ instance (PermCheckExtC ext, TransInfo info) =>
       ETrans_Term <$>
       applyMultiTransM (return $ globalOpenTerm "Prelude.modNat")
       [translateRWV e1, translateRWV e2]
-  
+
     -- Function handles: the expression part of a function handle has no
     -- computational content
     [nuMP| HandleLit _ |] -> return ETrans_Fun
-  
+
     -- Bitvectors
     [nuMP| BVLit w mb_bv |] ->
       return $ ETrans_Term $ bvLitOpenTerm (mbLift w) $ mbLift mb_bv
@@ -3659,12 +3675,12 @@ instance (PermCheckExtC ext, TransInfo info) =>
       (applyMultiTransM (return $ globalOpenTerm "Prelude.bvEq")
        [translate mb_w, translateRWV e,
         return (bvLitOpenTerm w (BV.zero w))])
-  
+
     -- Strings
     [nuMP| Expr.StringLit (UnicodeLiteral text) |] ->
       return $ ETrans_Term $ stringLitOpenTerm $
       mbLift text
-  
+
     -- Everything else is an error
     _ ->
       error ("Unhandled expression form: " ++
@@ -3799,12 +3815,12 @@ translateStmt loc mb_stmt m = case mbMatch mb_stmt of
        let ptrans = exprOutPerm e
        inExtTransM etrans $
          withPermStackM (:>: Member_Base) (:>: extPermTrans ptrans) m
-  
+
   [nuMP| TypedSetRegPermExpr _ e |] ->
     do etrans <- tpTransM $ translate e
        inExtTransM etrans $
          withPermStackM (:>: Member_Base) (:>: PTrans_Eq (extMb e)) m
-  
+
   [nuMP| stmt@(TypedCall _freg fun_perm _ gexprs args) |] ->
     do f_trans <- getTopPermM
        let f = case f_trans of
@@ -3839,14 +3855,14 @@ translateStmt loc mb_stmt m = case mbMatch mb_stmt of
              (const pctx)
              m)
            ret_val]
-  
+
   -- FIXME HERE: figure out why these asserts always translate to ite True
   [nuMP| TypedAssert e _ |] ->
     applyMultiTransM (return $ globalOpenTerm "Prelude.ite")
     [compReturnTypeM, translate1 e, m,
      mkErrorCompM ("Failed Assert at " ++
                    renderDoc (ppShortFileName (plSourceLoc loc)))]
-  
+
   [nuMP| TypedLLVMStmt stmt |] -> translateLLVMStmt stmt m
 
 
@@ -3860,31 +3876,31 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
     inExtTransM ETrans_LLVM $
     withPermStackM (:>: Member_Base) (:>: (PTrans_Eq $ extMb $
                                            fmap (PExpr_LLVMWord . PExpr_Var) x)) m
-  
+
   [nuMP| AssertLLVMWord reg _ |] ->
     inExtTransM (ETrans_Term $ natOpenTerm 0) $
     withPermStackM ((:>: Member_Base) . RL.tail)
     ((:>: (PTrans_Eq $ fmap (const $ PExpr_Nat 0) $ extMb reg)) . RL.tail)
     m
-  
+
   [nuMP| AssertLLVMPtr _ |] ->
     inExtTransM ETrans_Unit $
     withPermStackM RL.tail RL.tail m
-  
+
   [nuMP| DestructLLVMWord _ e |] ->
     translate e >>= \etrans ->
     inExtTransM etrans $
     withPermStackM ((:>: Member_Base) . RL.tail)
     ((:>: (PTrans_Eq $ extMb e)) . RL.tail)
     m
-  
+
   [nuMP| OffsetLLVMValue x off |] ->
     inExtTransM ETrans_LLVM $
     withPermStackM (:>: Member_Base)
     (:>: (PTrans_Eq $ extMb $
           mbMap2 PExpr_LLVMOffset (fmap typedRegVar x) off))
     m
-  
+
   [nuMP| TypedLLVMLoad _ (mb_fp :: LLVMFieldPerm w sz)
                        (_ :: DistPerms ps) cur_perms |] ->
     let prx_l = mbLifetimeCurrentPermsProxies cur_perms
@@ -3908,7 +3924,7 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
                               fmap (const $ nu $ \ret -> PExpr_Var ret) mb_fp)]
        :>: p_ret) pctx_l)
     m
-  
+
   [nuMP| TypedLLVMStore _ (mb_fp :: LLVMFieldPerm w sz) mb_e
                         (_ :: DistPerms ps) cur_perms |] ->
     let prx_l = mbLifetimeCurrentPermsProxies cur_perms
@@ -3926,7 +3942,7 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
                              (PTrans_Eq $ extMb mb_e)])
       pctx_l)
     m
-  
+
   [nuMP| TypedLLVMAlloca _ (mb_fperm :: LLVMFramePerm w) mb_sz |] ->
     let sz = mbLift mb_sz
         w :: Proxy w = Proxy in
@@ -3941,18 +3957,18 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
                        \(_ :>: ret) fperm -> (PExpr_Var ret, sz):fperm]
       :>: typeTransF ptrans_tp [])
     m
-  
+
   [nuMP| TypedLLVMCreateFrame |] ->
     withKnownNat ?ptrWidth $
     inExtTransM ETrans_LLVMFrame $
     withPermStackM (:>: Member_Base)
     (:>: PTrans_Conj [APTrans_LLVMFrame $ fmap (const []) (extMb mb_stmt)])
     m
-  
+
   [nuMP| TypedLLVMDeleteFrame _ _ _ |] ->
     inExtTransM ETrans_Unit $
     withPermStackM (const MNil) (const MNil) m
-  
+
   [nuMP| TypedLLVMLoadHandle _ tp _ |] ->
     inExtTransM ETrans_Fun $
     withPermStackM ((:>: Member_Base) . RL.tail)
@@ -3962,7 +3978,7 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
         _ -> error ("translateLLVMStmt: TypedLLVMLoadHandle: "
                     ++ "unexpected function permission type"))
     m
-  
+
   [nuMP| TypedLLVMResolveGlobal gsym (p :: ValuePerm (LLVMPointerType w))|] ->
     withKnownNat ?ptrWidth $
     inExtTransM ETrans_LLVM $
@@ -3975,7 +3991,7 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
                            ++ globalSymbolName (mbLift gsym))
          Just (_, ts) ->
            withPermStackM (:>: Member_Base) (:>: typeTransF ptrans ts) m
-  
+
   [nuMP| TypedLLVMIte _ mb_r1 _ _ |] ->
     inExtTransM ETrans_LLVM $
     do b <- translate1 $ extMb mb_r1
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Token.hs b/heapster-saw/src/Verifier/SAW/Heapster/Token.hs
index 7c007402a2..4f342923cf 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Token.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Token.hs
@@ -51,6 +51,7 @@ data Token
   | TLifetime           -- ^ keyword @lifetime@
   | TLOwned             -- ^ keyword @lowned@
   | TLCurrent           -- ^ keyword @lcurrent@
+  | TLFinished          -- ^ keyword @lfinished@
   | TRWModality         -- ^ keyword @rwmodality@
   | TPermList           -- ^ keyword @permlist@
   | TStruct             -- ^ keyword @struct@
@@ -130,6 +131,7 @@ describeToken t =
     TLifetime           -> "keyword 'lifetime'"
     TLOwned             -> "keyword 'lowned'"
     TLCurrent           -> "keyword 'lcurrent'"
+    TLFinished          -> "keyword 'lfinished'"
     TRWModality         -> "keyword 'rwmodality'"
     TPermList           -> "keyword 'permlist'"
     TStruct             -> "keyword 'struct'"
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
index 2579b458b5..b0cb527e98 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
@@ -603,11 +603,13 @@ tcBlockAtomic e = tcError (pos e) "Expected llvmblock perm"
 
 -- | Check a lifetime permission literal
 tcLifetimeAtomic :: AstExpr -> Tc (AtomicPerm LifetimeType)
-tcLifetimeAtomic (ExLOwned _ x y) =
+tcLifetimeAtomic (ExLOwned _ ls x y) =
   do Some x' <- tcLOwnedPerms x
      Some y' <- tcLOwnedPerms y
-     pure (Perm_LOwned x' y')
+     ls' <- mapM tcKExpr ls
+     pure (Perm_LOwned ls' x' y')
 tcLifetimeAtomic (ExLCurrent _ l) = Perm_LCurrent <$> tcOptLifetime l
+tcLifetimeAtomic (ExLFinished _) = return Perm_LFinished
 tcLifetimeAtomic e = tcError (pos e) "Expected lifetime perm"
 
 -- | Helper for lowned permission checking
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs
index c0d553162e..5716636ad2 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs
@@ -69,8 +69,9 @@ data AstExpr
   | ExLessEqual Pos AstExpr AstExpr -- ^ less-than or equal-to bitvector proposition
 
   | ExEq Pos AstExpr            -- ^ equal permission
-  | ExLOwned Pos [(Located String, AstExpr)] [(Located String, AstExpr)] -- ^ owned permission
+  | ExLOwned Pos [AstExpr] [(Located String, AstExpr)] [(Located String, AstExpr)] -- ^ owned permission
   | ExLCurrent Pos (Maybe AstExpr) -- ^ current permission
+  | ExLFinished Pos -- ^ finished permission
   | ExShape Pos AstExpr -- ^ shape literal
   | ExFree Pos AstExpr -- ^ free literal
   | ExPtr Pos (Maybe AstExpr) AstExpr AstExpr (Maybe AstExpr) AstExpr -- ^ pointer permission
@@ -106,8 +107,9 @@ instance HasPos AstExpr where
   pos (ExNotEqual   p _ _      ) = p
   pos (ExLessThan   p _ _      ) = p
   pos (ExLessEqual  p _ _      ) = p
-  pos (ExLOwned     p _ _      ) = p
+  pos (ExLOwned     p _ _ _    ) = p
   pos (ExLCurrent   p _        ) = p
+  pos (ExLFinished  p          ) = p
   pos (ExShape      p _        ) = p
   pos (ExFree       p _        ) = p
   pos (ExPtr        p _ _ _ _ _) = p