diff --git a/heapster-saw/heapster-saw.cabal b/heapster-saw/heapster-saw.cabal
index c8d2a8c1cf..90a7e4f4bf 100644
--- a/heapster-saw/heapster-saw.cabal
+++ b/heapster-saw/heapster-saw.cabal
@@ -37,6 +37,9 @@ library
     filepath,
     language-rust,
     hobbits ^>= 1.4,
+    aeson ^>= 1.5,
+    th-abstraction,
+    template-haskell
   hs-source-dirs: src
   build-tool-depends:
     alex:alex,
@@ -44,10 +47,12 @@ library
   exposed-modules:
     Verifier.SAW.Heapster.CruUtil
     Verifier.SAW.Heapster.GenMonad
+    Verifier.SAW.Heapster.IDESupport
     Verifier.SAW.Heapster.Implication
     Verifier.SAW.Heapster.IRTTranslation
     Verifier.SAW.Heapster.Lexer
     Verifier.SAW.Heapster.Located
+    Verifier.SAW.Heapster.JSONExport
     Verifier.SAW.Heapster.ParsedCtx
     Verifier.SAW.Heapster.Parser
     Verifier.SAW.Heapster.Permissions
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
index 6f9c36aab7..4ef922a0f2 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
@@ -23,6 +23,7 @@ import Data.Text (Text)
 import qualified Data.Text as Text
 import Data.Reflection
 import Data.List.NonEmpty (NonEmpty(..))
+import Data.Functor.Constant
 import Data.ByteString
 import Numeric
 import Numeric.Natural
@@ -564,6 +565,15 @@ instance Liftable (KnownReprObj f a) where
 instance LiftableAny1 (KnownReprObj f) where
   mbLiftAny1 = mbLift
 
+instance Liftable a => LiftableAny1 (Constant a) where
+  mbLiftAny1 = mbLift
+
+instance Liftable a => Liftable (Constant a b) where
+  mbLift (mbMatch -> [nuMP| Data.Functor.Constant.Constant x |]) = Data.Functor.Constant.Constant (mbLift x)
+
+instance (Liftable a, Liftable b, Liftable c) => Liftable (a,b,c) where
+  mbLift (mbMatch -> [nuMP| (x,y,z) |]) = (mbLift x, mbLift y, mbLift z)
+
 -- FIXME: this change for issue #28 requires ClosableAny1 to be exported from
 -- Hobbits
 {-
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs b/heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs
index 7ac7aa75b6..54bde8429e 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs
@@ -8,17 +8,19 @@ module Verifier.SAW.Heapster.GenMonad (
   -- * Core definitions
   GenStateContT(..), (>>>=), (>>>),
   -- * Continuation operations
-  gcaptureCC, gmapRet, gabortM, gparallel, gopenBinding,
+  gcaptureCC, gmapRet, gabortM, gparallel, startBinding, startBinding', gopenBinding, gopenBinding',
   -- * State operations
   gmodify,
   -- * Transformations
   addReader,
   ) where
 
-import Data.Binding.Hobbits ( nuMultiWithElim1, Mb, Name, RAssign )
+import Data.Binding.Hobbits ( nuMulti, nuMultiWithElim1, Mb, Name, RAssign )
 import Control.Monad.State ( ap, MonadState(get, put) )
 import Control.Monad.Trans.Class ( MonadTrans(lift) )
 import Control.Monad.Trans.Reader
+import Data.Proxy
+import Verifier.SAW.Heapster.NamedMb
 
 -- | The generalized state-continuation monad
 newtype GenStateContT s1 r1 s2 r2 m a = GenStateContT {
@@ -107,6 +109,30 @@ gopenBinding f_ret mb_a =
   f_ret $ flip nuMultiWithElim1 mb_a $ \names a ->
   k (names, a)
 
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+gopenBinding' ::
+  (Mb' ctx (m b1) -> m r2) ->
+  Mb' ctx b2 ->
+  GenStateContT s b1 s r2 m (RAssign Name ctx, b2)
+gopenBinding' f_ret mb_a =
+  gcaptureCC \k ->
+  f_ret $ flip nuMultiWithElim1' mb_a $ \names a ->
+  k (names, a)
+
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+startBinding ::
+  RAssign Proxy ctx ->
+  (Mb ctx (m r1) -> m r2) ->
+  GenStateContT s r1 s r2 m (RAssign Name ctx)
+startBinding tps f_ret = gcaptureCC (f_ret . nuMulti tps)
+
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+startBinding' ::
+  RAssign StringF ctx ->
+  (Mb' ctx (m r1) -> m r2) ->
+  GenStateContT s r1 s r2 m (RAssign Name ctx)
+startBinding' tps f_ret = gcaptureCC (f_ret . nuMulti' tps)
+
 addReader :: GenStateContT s1 r1 s2 r2 m a -> GenStateContT s1 r1 s2 r2 (ReaderT e m) a
 addReader (GenStateContT m) =
   GenStateContT \s2 k ->
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/IDESupport.hs b/heapster-saw/src/Verifier/SAW/Heapster/IDESupport.hs
new file mode 100644
index 0000000000..82f6d25e7a
--- /dev/null
+++ b/heapster-saw/src/Verifier/SAW/Heapster/IDESupport.hs
@@ -0,0 +1,330 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PolyKinds #-}
+module Verifier.SAW.Heapster.IDESupport where
+
+import Control.Monad.Reader
+  ( MonadReader (ask, local),
+    ReaderT (..),
+  )
+import Data.Aeson (ToJSON, Value, encodeFile)
+import Data.Binding.Hobbits
+  ( Liftable (..),
+    Mb,
+    NuMatching (..),
+    RList,
+    mbMatch,
+    nuMP,
+    nuMultiWithElim1,
+    unsafeMbTypeRepr,
+    Name,
+  )
+import Data.Maybe (catMaybes, listToMaybe, mapMaybe)
+import Data.Parameterized.Some (Some (..))
+import qualified Data.Text as T
+import qualified Data.Type.RList as RL
+import GHC.Generics (Generic)
+import Lang.Crucible.FunctionHandle
+import Lang.Crucible.Types (CrucibleType)
+import What4.FunctionName (FunctionName (functionName))
+import What4.ProgramLoc
+  ( Position (BinaryPos, InternalPos, OtherPos, SourcePos),
+    ProgramLoc (..),
+  )
+
+import Verifier.SAW.Heapster.CruUtil
+import Verifier.SAW.Heapster.Implication
+import Verifier.SAW.Heapster.Permissions
+import Verifier.SAW.Heapster.TypedCrucible
+import Verifier.SAW.Heapster.JSONExport(ppToJson)
+import Data.Type.RList (mapRAssign)
+import Data.Functor.Constant
+import Control.Monad.Writer
+import Data.Binding.Hobbits.NameMap (NameMap)
+import qualified Data.Binding.Hobbits.NameMap as NameMap
+import Verifier.SAW.Heapster.NamedMb
+
+-- | The entry point for dumping a Heapster environment to a file for IDE
+-- consumption.
+printIDEInfo :: PermEnv -> [Some SomeTypedCFG] -> FilePath -> PPInfo -> IO ()
+printIDEInfo _penv tcfgs file ppinfo =
+  encodeFile file $ IDELog (runWithLoc ppinfo tcfgs)
+
+
+type ExtractionM = ReaderT (PPInfo, ProgramLoc, String) (Writer [LogEntry])
+
+emit :: LogEntry -> ExtractionM ()
+emit entry = tell [entry]
+
+gather :: ExtractionM () -> ExtractionM [LogEntry]
+gather m = snd <$> listen m
+
+-- | A single entry in the IDE info dump log.  At a bare minimum, this must
+-- include a location and corresponding permission.  Once the basics are
+-- working, we can enrich the information we log.
+data LogEntry
+  = LogEntry
+      { leLocation :: String
+      , leEntryId :: LogEntryID
+      , leCallers :: [LogEntryID]
+      , leFunctionName :: String
+      , lePermissions :: [(String, String, Value)]
+      }
+  | LogError
+      { lerrLocation :: String
+      , lerrError :: String
+      , lerrFunctionName :: String
+      }
+  | LogImpl
+      { limplLocation :: String
+      , limplExport :: Value
+      , limplFunctionName :: String
+      }
+
+  deriving (Generic, Show)
+instance ToJSON LogEntry
+instance NuMatching LogEntry where
+  nuMatchingProof = unsafeMbTypeRepr
+instance Liftable LogEntry where
+  mbLift mb = case mbMatch mb of
+    [nuMP| LogEntry v w x y z |] -> 
+      LogEntry (mbLift v) (mbLift w) (mbLift x) (mbLift y) (mbLift z)
+    [nuMP| LogError x y z |] -> 
+      LogError (mbLift x) (mbLift y) (mbLift z)
+    [nuMP| LogImpl x y z |] -> 
+      LogImpl (mbLift x) (mbLift y) (mbLift z)
+
+data LogEntryID = LogEntryID
+  { leIdBlock :: Int
+  , leIdHeapster :: Int
+  }
+  deriving (Generic, Show)
+instance ToJSON LogEntryID
+instance NuMatching LogEntryID where
+  nuMatchingProof = unsafeMbTypeRepr 
+instance Liftable LogEntryID where
+  mbLift mb = case mbMatch mb of
+    [nuMP| LogEntryID x y |] -> LogEntryID (mbLift x) (mbLift y)
+
+-- | A complete IDE info dump log, which is just a sequence of entries.  Once
+-- the basics are working, we can enrich the information we log.
+newtype IDELog = IDELog {
+  lmfEntries :: [LogEntry]
+} deriving (Generic, Show)
+instance ToJSON IDELog
+
+
+class ExtractLogEntries a where
+  extractLogEntries :: a -> ExtractionM ()
+
+instance (PermCheckExtC ext)
+    => ExtractLogEntries
+         (TypedEntry TransPhase ext blocks tops ret args ghosts) where
+  extractLogEntries te = do
+    let loc = mbLift' $ fmap getFirstProgramLocTS (typedEntryBody te)
+    withLoc loc (mb'ExtractLogEntries (typedEntryBody te))
+    let entryId = mkLogEntryID $ typedEntryID te
+    let callers = callerIDs $ typedEntryCallers te
+    (ppi, _, fname) <- ask
+    let loc' = snd (ppLoc loc)
+    let debugNames = _mbNames (typedEntryBody te)
+    let insertNames ::
+          RL.RAssign Name (x :: RList CrucibleType) ->
+          RL.RAssign StringF x ->
+          NameMap (StringF :: CrucibleType -> *)->
+          NameMap (StringF :: CrucibleType -> *)
+        insertNames RL.MNil RL.MNil m = m
+        insertNames (ns RL.:>: n) (xs RL.:>: StringF name) m =
+          insertNames ns xs (NameMap.insert n (StringF name) m)
+        inputs = mbLift
+               $ flip nuMultiWithElim1 (typedEntryPermsIn te)
+               $ \ns body ->
+                 let ppi' = ppi { ppExprNames = insertNames ns debugNames (ppExprNames ppi) }
+                     f :: 
+                      (Pair StringF ValuePerm) x ->
+                      Constant (String, String, Value) x
+                     f (Pair (StringF name) vp) = Constant (name, permPrettyString ppi' vp, ppToJson ppi' vp)
+                 in RL.toList (mapRAssign f (zipRAssign debugNames body))
+    tell [LogEntry loc' entryId callers fname inputs]
+
+mkLogEntryID :: TypedEntryID blocks args -> LogEntryID
+mkLogEntryID = uncurry LogEntryID . entryIDIndices
+
+callerIDs :: [Some (TypedCallSite phase blocks tops args ghosts)] -> [LogEntryID]
+callerIDs = map $ \(Some tcs) -> case typedCallSiteID tcs of 
+    TypedCallSiteID tei _ _ _ -> mkLogEntryID tei
+
+data Pair f g x = Pair (f x) (g x)
+
+zipRAssign :: RL.RAssign f x -> RL.RAssign g x -> RL.RAssign (Pair f g) x
+zipRAssign RL.MNil RL.MNil = RL.MNil
+zipRAssign (xs RL.:>: x) (ys RL.:>: y) = zipRAssign xs ys RL.:>: Pair x y
+
+instance ExtractLogEntries (TypedStmtSeq ext blocks tops ret ps_in) where
+  extractLogEntries (TypedImplStmt (AnnotPermImpl _str pimpl)) =
+    -- fmap (setErrorMsg str) <$> extractLogEntries pimpl
+    extractLogEntries pimpl
+  extractLogEntries (TypedConsStmt loc _ _ rest) = do
+    withLoc loc $ mb'ExtractLogEntries rest
+  extractLogEntries (TypedTermStmt _ _) = pure ()
+
+instance ExtractLogEntries
+    (PermImpl (TypedStmtSeq ext blocks tops ret) ps_in) where
+  extractLogEntries (PermImpl_Step pi1 mbpis) = do
+    pi1Entries <- extractLogEntries pi1
+    pisEntries <- extractLogEntries mbpis
+    return $ pi1Entries <> pisEntries
+  extractLogEntries (PermImpl_Done stmts) = extractLogEntries stmts
+
+instance ExtractLogEntries (PermImpl1 ps_in ps_outs) where
+  extractLogEntries (Impl1_Fail err) =
+    do (_, loc, fname) <- ask
+       emit (LogError (snd (ppLoc loc)) (ppError err) fname)
+    -- The error message is available further up the stack, so we just leave it
+  extractLogEntries impl =
+    do (ppi, loc, fname) <- ask
+       emit (LogImpl (snd (ppLoc loc)) (ppToJson ppi impl) fname)
+
+instance ExtractLogEntries
+    (MbPermImpls (TypedStmtSeq ext blocks tops ret) ps_outs) where
+  extractLogEntries (MbPermImpls_Cons ctx mbpis pis) = do
+    mbExtractLogEntries ctx pis
+    extractLogEntries mbpis
+  extractLogEntries MbPermImpls_Nil = pure ()
+
+instance (PermCheckExtC ext)
+  => ExtractLogEntries (TypedCFG ext blocks ghosts inits ret) where
+    extractLogEntries tcfg = extractLogEntries $ tpcfgBlockMap tcfg
+
+instance (PermCheckExtC ext)
+  => ExtractLogEntries (TypedBlockMap TransPhase ext blocks tops ret) where
+  extractLogEntries tbm =
+    sequence_ $ RL.mapToList extractLogEntries tbm
+
+instance (PermCheckExtC ext)
+  => ExtractLogEntries (TypedBlock TransPhase ext blocks tops ret args) where
+    extractLogEntries tb =
+      mapM_ (\(Some te) -> extractLogEntries te) $ _typedBlockEntries tb
+
+mbExtractLogEntries
+  :: ExtractLogEntries a => CruCtx ctx -> Mb (ctx :: RList CrucibleType) a -> ExtractionM ()
+mbExtractLogEntries ctx mb_a =
+  ReaderT $ \(ppi, loc, fname) ->
+  tell $ mbLift $ flip nuMultiWithElim1 mb_a $ \ns x ->
+  let ppi' = ppInfoAddTypedExprNames ctx ns ppi in
+  execWriter $ runReaderT (extractLogEntries x) (ppi', loc, fname)
+
+mb'ExtractLogEntries
+  :: ExtractLogEntries a => Mb' (ctx :: RList CrucibleType) a -> ExtractionM ()
+mb'ExtractLogEntries mb_a =
+  ReaderT $ \(ppi, loc, fname) ->
+  tell $ mbLift $ flip nuMultiWithElim1 (_mbBinding mb_a) $ \ns x ->
+  let ppi' = ppInfoApplyAllocation ns (_mbNames mb_a) ppi in
+  execWriter $ runReaderT (extractLogEntries x) (ppi', loc, fname)
+
+typedStmtOutCtx :: TypedStmt ext rets ps_in ps_next -> CruCtx rets
+typedStmtOutCtx = error "FIXME: write typedStmtOutCtx"
+
+withLoc :: ProgramLoc -> ExtractionM a -> ExtractionM a
+withLoc loc = local (\(ppinfo, _, fname) -> (ppinfo, loc, fname))
+
+setErrorMsg :: String -> LogEntry -> LogEntry
+setErrorMsg msg le@LogError {} = le { lerrError = msg }
+setErrorMsg msg le@LogImpl {} =
+  LogError { lerrError = msg
+           , lerrLocation = limplLocation le
+           , lerrFunctionName = limplFunctionName le}
+setErrorMsg msg le@LogEntry {} =
+  LogError { lerrError = msg
+           , lerrLocation = leLocation le
+           , lerrFunctionName = leFunctionName le
+           }
+
+runWithLoc :: PPInfo -> [Some SomeTypedCFG] -> [LogEntry]
+runWithLoc ppi =
+  concatMap (runWithLocHelper ppi)
+  where
+    runWithLocHelper :: PPInfo -> Some SomeTypedCFG -> [LogEntry]
+    runWithLocHelper ppi' sstcfg = case sstcfg of
+      Some (SomeTypedCFG tcfg) -> do
+        let env = (ppi', getFirstProgramLoc tcfg, getFunctionName tcfg)
+        execWriter (runReaderT (extractLogEntries tcfg) env)
+
+getFunctionName :: TypedCFG ext blocks ghosts inits ret -> String
+getFunctionName tcfg = case tpcfgHandle tcfg of
+  TypedFnHandle _ handle -> show $ handleName handle
+
+getFirstProgramLoc
+  :: PermCheckExtC ext
+  => TypedCFG ext blocks ghosts inits ret -> ProgramLoc
+getFirstProgramLoc tcfg =
+  case listToMaybe $ catMaybes $
+         RL.mapToList getFirstProgramLocBM $ tpcfgBlockMap tcfg of
+    Just pl -> pl
+    _ -> error "Unable to get initial program location"
+
+getFirstProgramLocBM
+  :: PermCheckExtC ext
+  => TypedBlock TransPhase ext blocks tops ret ctx
+  -> Maybe ProgramLoc
+getFirstProgramLocBM block =
+  listToMaybe $ mapMaybe helper (_typedBlockEntries block)
+  where
+    helper
+      :: PermCheckExtC ext
+      => Some (TypedEntry TransPhase ext blocks tops ret ctx)
+      -> Maybe ProgramLoc
+    helper ste = case ste of
+      Some TypedEntry { typedEntryBody = stmts } ->
+        Just $ mbLift' $ fmap getFirstProgramLocTS stmts
+
+-- | From the sequence, get the first program location we encounter, which
+-- should correspond to the permissions for the entry point we want to log
+getFirstProgramLocTS :: PermCheckExtC ext
+  => TypedStmtSeq ext blocks tops ret ctx
+  -> ProgramLoc
+getFirstProgramLocTS (TypedImplStmt (AnnotPermImpl _ pis)) =
+  getFirstProgramLocPI pis
+getFirstProgramLocTS (TypedConsStmt loc _ _ _) = loc
+getFirstProgramLocTS (TypedTermStmt loc _) = loc
+
+getFirstProgramLocPI
+  :: PermCheckExtC ext
+  => PermImpl (TypedStmtSeq ext blocks tops ret) ctx
+  -> ProgramLoc
+getFirstProgramLocPI (PermImpl_Done stmts) = getFirstProgramLocTS stmts
+getFirstProgramLocPI (PermImpl_Step _ mbps) = getFirstProgramLocMBPI mbps
+
+getFirstProgramLocMBPI
+  :: PermCheckExtC ext
+  => MbPermImpls (TypedStmtSeq ext blocks tops ret) ctx
+  -> ProgramLoc
+getFirstProgramLocMBPI MbPermImpls_Nil =
+  error "Error finding program location for IDE log"
+getFirstProgramLocMBPI (MbPermImpls_Cons _ _ pis) =
+  mbLift $ fmap getFirstProgramLocPI pis
+
+-- | Print a `ProgramLoc` in a way that is useful for an IDE, i.e., machine
+-- readable
+ppLoc :: ProgramLoc -> (String, String)
+ppLoc pl =
+  let fnName = T.unpack $ functionName $ plFunction pl
+      locStr = ppPos $ plSourceLoc pl
+
+      ppPos (SourcePos file line column) =
+        T.unpack file <> ":" <> show line <> ":" <> show column
+      ppPos (BinaryPos _ _) = "<unknown binary pos>"
+      ppPos (OtherPos _) = "<unknown other pos>"
+      ppPos InternalPos = "<unknown internal pos>"
+  in (fnName, locStr)
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 37325ad95c..e1bb017c26 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -67,6 +67,7 @@ import GHC.Stack
 import Debug.Trace
 
 
+
 ----------------------------------------------------------------------
 -- * Equality Proofs
 ----------------------------------------------------------------------
@@ -307,6 +308,76 @@ unSomeEqProof (SomeEqProofCons some_eqp eq_step)
     UnSomeEqProof $ EqProofCons eqp eq_step
 
 
+----------------------------------------------------------------------
+-- * Implication Errors
+----------------------------------------------------------------------
+
+data ImplError where
+  GeneralError :: Doc ann -> ImplError
+  NoFrameInScopeError :: ImplError
+  ArrayStepError :: ImplError
+  MuUnfoldError :: ImplError
+  FunctionPermissionError :: ImplError
+  PartialSubstitutionError :: String -> Doc ann -> ImplError
+  LifetimeError :: LifetimeErrorType -> ImplError
+  MemBlockError :: Doc ann -> ImplError
+  EqualityProofError :: Doc ann -> Doc ann -> ImplError
+  InsufficientVariablesError :: Doc ann -> ImplError
+  ExistentialError :: Doc ann -> Doc ann -> ImplError
+  ImplVariableError 
+    :: Doc ann -> String 
+    -> (Doc ann, ExprVar tp) -> (Doc ann, ValuePerm tp) -> CruCtx vars 
+    -> DistPerms ps
+    -> ImplError
+
+data LifetimeErrorType where
+  EndLifetimeError :: LifetimeErrorType
+  ImplicationLifetimeError :: LifetimeErrorType
+  LifetimeCurrentError :: PP.Doc ann -> LifetimeErrorType
+
+instance SubstVar PermVarSubst m =>
+    Substable PermVarSubst ImplError m where
+  genSubst s mb_impl = case mbMatch mb_impl of
+    [nuMP| GeneralError doc |] -> 
+      return $ GeneralError $ mbLift doc
+    [nuMP| NoFrameInScopeError |] -> 
+      return NoFrameInScopeError
+    [nuMP| ArrayStepError |] -> 
+      return ArrayStepError
+    [nuMP| MuUnfoldError |] -> 
+      return MuUnfoldError
+    [nuMP| FunctionPermissionError |] -> 
+      return FunctionPermissionError
+    [nuMP| PartialSubstitutionError str doc |] -> 
+      return $ PartialSubstitutionError (mbLift str) (mbLift doc)
+    [nuMP| LifetimeError le |] -> 
+      return $ LifetimeError $ mbLift le
+    [nuMP| MemBlockError doc |] -> 
+      return $ MemBlockError (mbLift doc)
+    [nuMP| EqualityProofError docl docr |] -> 
+      return $ EqualityProofError (mbLift docl) (mbLift docr)
+    [nuMP| InsufficientVariablesError doc |] -> 
+      return $ InsufficientVariablesError $ mbLift doc
+    [nuMP| ExistentialError doc1 doc2 |] -> 
+      return $ ExistentialError (mbLift doc1) (mbLift doc2)
+    [nuMP| ImplVariableError doc f (xdoc, x) (pdoc, p) ctx mb_dp |] -> do
+      x' <- genSubst s x
+      p' <- genSubst s p
+      dp <- genSubst s mb_dp
+      return $ ImplVariableError (mbLift doc) (mbLift f) (mbLift xdoc, x') (mbLift pdoc, p') (mbLift ctx) dp
+   
+instance Liftable LifetimeErrorType where
+  mbLift e = case mbMatch e of
+    [nuMP| EndLifetimeError |] -> EndLifetimeError
+    [nuMP| ImplicationLifetimeError |] -> ImplicationLifetimeError
+    [nuMP| LifetimeCurrentError doc |] -> LifetimeCurrentError $ mbLift doc
+
+-- The reason this isn't just Show is to sort of future-proof things. For
+-- instance, we may want to dump a limited amount of information to stdout, but
+-- something more comprehensive to a log for an IDE.
+class ErrorPretty a where
+  ppError :: a -> String
+
 ----------------------------------------------------------------------
 -- * Permission Implications
 ----------------------------------------------------------------------
@@ -1161,7 +1232,7 @@ data PermImpl1 ps_in ps_outs where
   -- the failure, which is a proof of 0 disjuncts:
   --
   -- > ps -o .
-  Impl1_Fail :: String -> PermImpl1 ps RNil
+  Impl1_Fail :: ImplError -> PermImpl1 ps RNil
 
   -- | Catch any failure in the first branch by calling the second, passing the
   -- same input permissions to both branches:
@@ -1306,16 +1377,6 @@ idLocalPermImpl = LocalPermImpl $ PermImpl_Done $ LocalImplRet Refl
 
 -- type IsLLVMPointerTypeList w ps = RAssign ((:~:) (LLVMPointerType w)) ps
 
-$(mkNuMatching [t| forall a. EqPerm a |])
-$(mkNuMatching [t| forall ps a. NuMatching a => EqProofStep ps a |])
-$(mkNuMatching [t| forall ps a. NuMatching a => EqProof ps a |])
-$(mkNuMatching [t| forall ps_in ps_out. SimplImpl ps_in ps_out |])
-$(mkNuMatching [t| forall ps_in ps_outs. PermImpl1 ps_in ps_outs |])
-$(mkNuMatching [t| forall r bs_pss. NuMatchingAny1 r => MbPermImpls r bs_pss |])
-$(mkNuMatching [t| forall r ps. NuMatchingAny1 r => PermImpl r ps |])
-$(mkNuMatching [t| forall ps_in ps_out. LocalPermImpl ps_in ps_out |])
-$(mkNuMatching [t| forall ps ps'. LocalImplRet ps ps' |])
-
 instance NuMatchingAny1 EqPerm where
   nuMatchingAny1Proof = nuMatchingProof
 
@@ -1378,8 +1439,8 @@ permImplStep (Impl1_ElimOr _ _ _) (MbPermImpls_Cons _
                                    (MbPermImpls_Cons _ MbPermImpls_Nil
                                     (matchMbImplFail -> Just msg1))
                                    (matchMbImplFail -> Just msg2)) =
-  PermImpl_Step (Impl1_Fail
-                 (msg1 ++ "\n\n--------------------\n\n" ++ msg2))
+  PermImpl_Step (Impl1_Fail $ GeneralError $ pretty
+                  (msg1 ++ "\n\n--------------------\n\n" ++ msg2))
   MbPermImpls_Nil
 
 -- Default case: just apply PermImpl_Step
@@ -1395,7 +1456,7 @@ permImplStepUnary :: NuMatchingAny1 r =>
 
 -- If the continuation implication is a failure, percolate it up
 permImplStepUnary _ (MbPermImpls_Cons _ _ (matchMbImplFail -> Just msg)) =
-  PermImpl_Step (Impl1_Fail msg) MbPermImpls_Nil
+  PermImpl_Step (Impl1_Fail $ GeneralError $ pretty msg) MbPermImpls_Nil
 
 -- If the continuation implication is a catch with a failure on the right-hand
 -- side, percolate up the catch
@@ -1419,7 +1480,7 @@ permImplStepUnary impl1 mb_impls = PermImpl_Step impl1 mb_impls
 -- 'NuMatchingAny1' constraint on the @r@ variable
 matchMbImplFail :: NuMatchingAny1 r => Mb ctx (PermImpl r ps) -> Maybe String
 matchMbImplFail mb_impl = case mbMatch mb_impl of
-  [nuMP| PermImpl_Step (Impl1_Fail msg) _ |] -> Just $ mbLift msg
+  [nuMP| PermImpl_Step (Impl1_Fail err) _ |] -> Just $ mbLift $ fmap ppError err
   _ -> Nothing
 
 -- | Pattern-matchin an implication inside a binding to see if it is a catch
@@ -1447,7 +1508,9 @@ permImplCatch pimpl (PermImpl_Step (Impl1_Fail _) _)
   | pruneFailingBranches = pimpl
 permImplCatch (PermImpl_Step (Impl1_Fail str1) _) (PermImpl_Step
                                                    (Impl1_Fail str2) mb_impls) =
-  PermImpl_Step (Impl1_Fail (str1 ++ "\n\n--------------------\n\n" ++ str2)) mb_impls
+  PermImpl_Step (Impl1_Fail $ GeneralError $ 
+      pretty (ppError str1 ++ "\n\n--------------------\n\n" ++ ppError str2)) 
+    mb_impls
 permImplCatch pimpl1@(PermImpl_Step (Impl1_Fail _) _) pimpl2 =
   permImplCatch pimpl2 pimpl1
 permImplCatch (PermImpl_Step Impl1_Catch
@@ -2542,7 +2605,7 @@ instance SubstVar PermVarSubst m =>
 instance SubstVar PermVarSubst m =>
          Substable PermVarSubst (PermImpl1 ps_in ps_out) m where
   genSubst s mb_impl = case mbMatch mb_impl of
-    [nuMP| Impl1_Fail str |] -> return (Impl1_Fail $ mbLift str)
+    [nuMP| Impl1_Fail err |] -> Impl1_Fail <$> genSubst s err
     [nuMP| Impl1_Catch |] -> return Impl1_Catch
     [nuMP| Impl1_Push x p |] ->
       Impl1_Push <$> genSubst s x <*> genSubst s p
@@ -2779,12 +2842,11 @@ partialSubstForceM :: (NuMatchingAny1 r, PermPretty a,
                       Mb vars a -> String -> ImplM vars s r ps ps a
 partialSubstForceM mb_e caller =
   do psubst <- getPSubst
-     case partialSubst psubst mb_e of
-       Just e -> pure e
-       Nothing ->
-         implTraceM (\i -> sep [pretty ("Incomplete susbtitution in " ++ caller
-                                        ++ " for:"),
-                                permPretty i mb_e]) >>= implFailM
+     use implStatePPInfo >>>= \ppinfo ->
+       case partialSubst psubst mb_e of
+         Just e -> pure e
+         Nothing ->
+           implFailM $ PartialSubstitutionError caller (permPretty ppinfo mb_e)
 
 -- | Modify the current partial substitution
 modifyPSubst :: (PartialSubst vars -> PartialSubst vars) ->
@@ -2850,7 +2912,7 @@ implRecFlagCaseM m1 m2 =
 implSetRecRecurseRightM :: NuMatchingAny1 r => ImplM vars s r ps ps ()
 implSetRecRecurseRightM =
   use implStateRecRecurseFlag >>= \case
-    RecLeft -> implFailMsgM "Tried to unfold a mu on the right after unfolding on the left"
+    RecLeft -> implFailM MuUnfoldError
     _ -> implStateRecRecurseFlag .= RecRight
 
 -- | Set the recursive recursion flag to indicate recursion on the left, or fail
@@ -2859,7 +2921,7 @@ implSetRecRecurseLeftM :: NuMatchingAny1 r => ImplM vars s r ps ps ()
 implSetRecRecurseLeftM =
   use implStateRecRecurseFlag >>= \case
     RecRight ->
-      implFailMsgM "Tried to unfold a mu on the left after unfolding on the right"
+      implFailM MuUnfoldError
     _ -> implStateRecRecurseFlag .= RecLeft
 
 -- | Look up the 'NamedPerm' structure for a named permssion
@@ -2943,6 +3005,45 @@ implSetNameTypes (ns :>: n) (CruCtxCons tps tp) =
      implStatePerms     %= initVarPerm n
      implSetNameTypes ns tps
 
+-- | TODO: Move this in to Hobbits
+nameMapFind 
+  :: (forall tp. f tp -> Bool) 
+  -> NameMap f 
+  -> Maybe (Some (Product Name f))
+nameMapFind predicate nm = 
+  case find (\(NameAndElem _ f) -> predicate f) $ NameMap.assocs nm of
+    Just (NameAndElem name f) -> Just $ Some $ Pair name f
+    Nothing -> Nothing
+
+-- | Traverse a permissions to determine whether it refers to a particular variable.
+permContainsVar :: ExprVar a -> ValuePerm b -> Bool
+permContainsVar ev (ValPerm_Eq pe) = permExprContainsVar ev pe
+permContainsVar ev (ValPerm_Or l r) = permContainsVar ev l || permContainsVar ev r
+permContainsVar ev (ValPerm_Exists vp) = mbLift $ fmap (permContainsVar ev) vp
+permContainsVar ev (ValPerm_Named _ pe _) = 
+  or $ RL.mapToList (permExprContainsVar ev) pe
+permContainsVar _  (ValPerm_Var _ _) = False
+permContainsVar ev (ValPerm_Conj as) = any atomicHelper as
+  where
+    atomicHelper :: AtomicPerm a -> Bool
+    atomicHelper (Perm_NamedConj _ perms _) = 
+      or $ RL.mapToList (permExprContainsVar ev) perms
+    atomicHelper _ = False
+
+
+permExprContainsVar :: ExprVar a -> PermExpr b -> Bool
+permExprContainsVar ev1 (PExpr_Var ev2) = case testEquality ev1 ev2 of
+  Just Refl -> ev1 == ev2
+  Nothing -> False
+permExprContainsVar _ _ = False
+
+findPermsContainingVar :: ExprVar tp -> ImplM vars s r ps ps (Some DistPerms)
+findPermsContainingVar x = 
+  getPerms >>>= \perms ->
+    case nameMapFind (permContainsVar x) (view varPermMap perms) of
+      Just (Some (Pair y p)) -> findPermsContainingVar y >>>= \(Some dps) ->
+        return $ Some $ DistPermsCons dps y p
+      Nothing -> return $ Some DistPermsNil
 
 ----------------------------------------------------------------------
 -- * The Permission Implication Rules as Monadic Operations
@@ -2982,18 +3083,6 @@ implApplyImpl1 impl1 mb_ms =
         implSetNameTypes ns ctx >>>
         f ns)
 
--- | Emit debugging output using the current 'PPInfo' if the 'implStateDoTrace'
--- flag is set
-implTraceM :: (PPInfo -> PP.Doc ann) -> ImplM vars s r ps ps String
-implTraceM f =
-  do do_trace <- use implStateDoTrace
-     doc <- uses implStatePPInfo f
-     let str = renderDoc doc
-     fn do_trace str (pure str)
-  where
-    fn True  = trace
-    fn False = const id
-
 -- | Run an 'ImplM' computation with 'implStateDoTrace' temporarily disabled
 implWithoutTracingM :: ImplM vars s r ps_out ps_in a ->
                        ImplM vars s r ps_out ps_in a
@@ -3004,18 +3093,6 @@ implWithoutTracingM m =
   (implStateDoTrace .= saved) >>
   pure a
 
--- | Terminate the current proof branch with a failure
-implFailM :: NuMatchingAny1 r => String -> ImplM vars s r ps_any ps a
-implFailM str =
-  use implStateFailPrefix >>>= \prefix ->
-  implTraceM (const $ pretty (prefix ++ "Implication failed")) >>>
-  implApplyImpl1 (Impl1_Fail (prefix ++ str)) MNil
-
--- | Call 'implFailM' and also output a debugging message
-implFailMsgM :: NuMatchingAny1 r => String -> ImplM vars s r ps_any ps a
-implFailMsgM msg =
-  implTraceM (const $ pretty msg) >>>= implFailM
-
 -- | Pretty print an implication @x:p -o (vars).p'@
 ppImpl :: PPInfo -> ExprVar tp -> ValuePerm tp ->
           Mb (vars :: RList CrucibleType) (ValuePerm tp) -> PP.Doc ann
@@ -3024,15 +3101,6 @@ ppImpl i x p mb_p =
        PP.pretty "-o",
        PP.group (PP.align (permPretty i mb_p))]
 
--- | Terminate the current proof branch with a failure proving @x:p -o mb_p@
-implFailVarM :: NuMatchingAny1 r => String -> ExprVar tp -> ValuePerm tp ->
-                Mb vars (ValuePerm tp) -> ImplM vars s r ps_any ps a
-implFailVarM f x p mb_p =
-  implTraceM (\i ->
-               sep [pretty f <> colon <+> pretty "Could not prove",
-                    ppImpl i x p mb_p]) >>>=
-  implFailM
-
 -- | Produce a branching proof tree that performs the first implication and, if
 -- that one fails, falls back on the second. If 'pruneFailingBranches' is set,
 -- failing branches are pruned.
@@ -3264,7 +3332,7 @@ implElimLLVMBlockToEq x bp =
   pure y
 
 -- | Try to prove a proposition about bitvectors dynamically, failing as in
--- 'implFailM' if the proposition does not hold
+-- 'implFailM if the proposition does not hold
 implTryProveBVProp :: (1 <= w, KnownNat w, NuMatchingAny1 r) =>
                       ExprVar (LLVMPointerType w) -> BVProp w ->
                       ImplM vars s r (ps :> LLVMPointerType w) ps ()
@@ -3729,7 +3797,7 @@ implEndLifetimeM ps l ps_in ps_out@(lownedPermsToDistPerms -> Just dps_out)
     implSimplM ps (SImpl_EndLifetime l ps_in ps_out) >>>
     implTraceM (\i -> pretty "Ending lifetime:" <+> permPretty i l) >>>
     recombinePermsPartial ps (DistPermsCons dps_out l ValPerm_LFinished)
-implEndLifetimeM _ _ _ _ = implFailM "implEndLifetimeM: lownedPermsToDistPerms"
+implEndLifetimeM _ _ _ _ = implFailM (LifetimeError EndLifetimeError)
 
 -- | 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. Assume
@@ -4103,9 +4171,8 @@ implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
 
 -- If none of the above cases matched, we cannot eliminate, so fail
 implElimLLVMBlock _ bp =
-  implTraceM (\i -> pretty "Could not eliminate permission" <+>
-                    permPretty i (Perm_LLVMBlock bp)) >>>=
-  implFailM
+  use implStatePPInfo >>>= \ppinfo ->
+    implFailM $ MemBlockError $ permPretty ppinfo (Perm_LLVMBlock bp)
 
 
 -- | Assume the top of the stack contains @x:ps@, which are all the permissions
@@ -4199,9 +4266,8 @@ getLifetimeCurrentPerms (PExpr_Var l) =
       case some_cur_perms of
         Some cur_perms -> pure $ Some $ CurrentTransPerms cur_perms l
     _ ->
-      implTraceM (\i -> pretty "Could not prove lifetime is current:" <+>
-                        permPretty i l) >>=
-      implFailM
+      use implStatePPInfo >>>= \ppinfo ->
+        implFailM $ LifetimeError (LifetimeCurrentError $ permPretty ppinfo l)
 
 -- | Prove the permissions represented by a 'LifetimeCurrentPerms'
 proveLifetimeCurrent :: NuMatchingAny1 r => LifetimeCurrentPerms ps_l ->
@@ -4426,16 +4492,6 @@ recombineLifetimeCurrentPerms (CurrentTransPerms cur_perms l) =
 -- * Proving Equalities
 ----------------------------------------------------------------------
 
--- | Fail when trying to prove an equality
-proveEqFail :: (NuMatchingAny1 r, PermPretty (f a)) => f a -> Mb vars (f a) ->
-               ImplM vars s r ps ps any
-proveEqFail e mb_e =
-  implTraceM (\i ->
-               sep [pretty "proveEq" <> colon <+> pretty "Could not prove",
-                    sep [permPretty i e <+>
-                         pretty "=" <+> permPretty i mb_e]]) >>>=
-  implFailM
-
 -- | Typeclass for the generic function that tries to extend the current partial
 -- substitution to unify an expression with an expression pattern and returns a
 -- proof of the equality on success
@@ -4472,7 +4528,11 @@ instance ProveEq (LLVMFramePerm w) where
       do eqp1 <- proveEq e mb_e
          eqp2 <- proveEq fperms mb_fperms
          pure (liftA2 (\x y -> (x,i):y) eqp1 eqp2)
-  proveEq perms mb = proveEqFail perms mb
+  proveEq perms mb = 
+    use implStatePPInfo >>>= \ppinfo ->
+      implFailM $ EqualityProofError 
+                    (permPretty ppinfo perms) 
+                    (permPretty ppinfo mb)
 
 instance ProveEq (LLVMBlockPerm w) where
   proveEq bp mb_bp =
@@ -4546,7 +4606,11 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
           Just _ -> proveEqH psubst e mb_e
           Nothing -> getVarEqPerm y >>= \case
             Just _ -> proveEqH psubst e mb_e
-            Nothing -> proveEqFail e mb_e
+            Nothing -> 
+              use implStatePPInfo >>>= \ppinfo ->
+                implFailM $ EqualityProofError 
+                              (permPretty ppinfo e)
+                              (permPretty ppinfo mb_e)
 
   -- To prove x=e, try to see if x:eq(e') and proceed by transitivity
   (PExpr_Var x, _) ->
@@ -4554,7 +4618,11 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
     Just e' ->
       proveEq e' mb_e >>= \eqp2 ->
       pure (someEqProofTrans (someEqProof1 x e' True) eqp2)
-    Nothing -> proveEqFail e mb_e
+    Nothing ->
+      use implStatePPInfo >>>= \ppinfo ->
+      implFailM $ EqualityProofError 
+                    (permPretty ppinfo e)
+                    (permPretty ppinfo mb_e)
 
   -- To prove e=x, try to see if x:eq(e') and proceed by transitivity
   (_, [nuMP| PExpr_Var z |])
@@ -4563,7 +4631,11 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
         Just e' ->
           proveEq e (fmap (const e') mb_e) >>= \eqp ->
           pure (someEqProofTrans eqp (someEqProof1 x e' False))
-        Nothing -> proveEqFail e mb_e
+        Nothing ->
+          use implStatePPInfo >>>= \ppinfo ->
+          implFailM $ EqualityProofError 
+                        (permPretty ppinfo e)
+                        (permPretty ppinfo mb_e)
 
   -- FIXME: if proving word(e1)=word(e2) for ground e2, we could add an assertion
   -- that e1=e2 using a BVProp_Eq
@@ -4583,7 +4655,10 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   -- FIXME: add cases to prove struct(es1)=struct(es2)
 
   -- Otherwise give up!
-  _ -> proveEqFail e mb_e
+  _ -> use implStatePPInfo >>>= \ppinfo ->
+         implFailM $ EqualityProofError 
+                       (permPretty ppinfo e)
+                       (permPretty ppinfo mb_e)
 
 
 -- | Build a proof on the top of the stack that @x:eq(e)@. Assume that all @x@
@@ -5255,7 +5330,7 @@ proveVarLLVMArray_ArrayStep x ps ap i ap_lhs
 
 -- Otherwise we don't know what to do so we fail
 proveVarLLVMArray_ArrayStep _x _ps _ap _i _ap_lhs =
-  implFailMsgM "proveVarLLVMArray_ArrayStep"
+  implFailM ArrayStepError
 
 
 ----------------------------------------------------------------------
@@ -6322,7 +6397,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
              lownedPermsToDistPerms ps_inR, lownedPermsToDistPerms ps_outR) of
           (Just dps_inL, Just dps_outL, Just dps_inR, Just dps_outR) ->
             pure (dps_inL, dps_outL, dps_inR, dps_outR)
-          _ -> implFailMsgM "proveVarAtomicImpl: lownedPermsToDistPerms")
+          _ -> implFailM (LifetimeError ImplicationLifetimeError))
       >>>= \(dps_inL, dps_outL, dps_inR, dps_outR) ->
       localProveVars (RL.append ps1 dps_inR) dps_inL >>>= \impl_in ->
       localProveVars (RL.append ps2 dps_outL) dps_outR >>>= \impl_out ->
@@ -6461,12 +6536,9 @@ proveVarConjImpl x ps mb_ps =
                            mb_ps' mb_p) "proveVarConjImpl") >>>= \(ps',p) ->
       implInsertConjM x p ps' i
     Nothing ->
-      implTraceM
-      (\i ->
-        sep [PP.fillSep [PP.pretty
-             "Could not determine enough variables to prove permissions:",
-             permPretty i (fmap ValPerm_Conj mb_ps)]]) >>>=
-      implFailM
+      use implStatePPInfo >>>= \ppinfo ->
+        implFailM $ InsufficientVariablesError $ 
+                      permPretty ppinfo (fmap ValPerm_Conj mb_ps)
 
 
 ----------------------------------------------------------------------
@@ -6786,15 +6858,14 @@ proveExVarImpl _ mb_x mb_p@(mbMatch -> [nuMP| ValPerm_Conj [Perm_LLVMFrame _] |]
         getVarVarM memb >>>= \n' ->
         proveVarImplInt n' mb_p >>> pure n'
       Nothing ->
-        implFailMsgM "proveExVarImpl: No LLVM frame pointer in scope"
+        implFailM NoFrameInScopeError
 
 -- Otherwise we fail
 proveExVarImpl _ mb_x mb_p =
-  implTraceM (\i -> pretty "proveExVarImpl: existential variable" <+>
-                    permPretty i mb_x <+>
-                    pretty "not resolved when trying to prove:" <> softline <>
-                    permPretty i mb_p) >>>=
-  implFailM
+  use implStatePPInfo >>>= \ppinfo ->
+    implFailM $ ExistentialError 
+                  (permPretty ppinfo mb_x)
+                  (permPretty ppinfo mb_p)
 
 
 ----------------------------------------------------------------------
@@ -6947,12 +7018,9 @@ proveVarsImplAppendInt ps =
       proveVarsImplAppendInt (mbMap2 appendDistPerms ps1 ps2) >>>
       implMoveUpM cur_perms (mbDistPermsToProxies ps1) x (mbDistPermsToProxies ps2)
     _ ->
-      implTraceM
-      (\i ->
-        sep [PP.fillSep [PP.pretty
-             "Could not determine enough variables to prove permissions:",
-             permPretty i ps]]) >>>=
-      implFailM
+      use implStatePPInfo >>>= \ppinfo ->
+        implFailM $ InsufficientVariablesError $
+                      permPretty ppinfo ps
 
 -- | Prove a list of existentially-quantified distinguished permissions and put
 -- those proofs onto the stack. This is the same as 'proveVarsImplAppendInt'
@@ -7018,7 +7086,8 @@ implEndLifetimeRecM l =
   _ ->
     implTraceM (\i ->
                  pretty "implEndLifetimeRecM: could not end lifetime: " <>
-                 permPretty i l) >>>= implFailM
+                 permPretty i l) >>>
+    implFailM (LifetimeError EndLifetimeError)
 
 
 -- | Prove a list of existentially-quantified distinguished permissions, adding
@@ -7079,3 +7148,99 @@ proveVarsImplVarEVars mb_ps =
 proveVarImpl :: NuMatchingAny1 r => ExprVar a -> Mb vars (ValuePerm a) ->
                 ImplM vars s r (ps :> a) ps ()
 proveVarImpl x mb_p = proveVarsImplAppend $ fmap (distPerms1 x) mb_p
+
+
+-- | Terminate the current proof branch with a failure
+implFailM :: NuMatchingAny1 r => ImplError -> ImplM vars s r ps_any ps a
+implFailM err =
+  use implStateFailPrefix >>>= \prefix ->
+    implTraceM (const $ pretty $ prefix <> ppError err) >>> 
+    implApplyImpl1 (Impl1_Fail err) MNil
+
+-- | Terminate the current proof branch with a failure proving @x:p -o mb_p@
+implFailVarM :: NuMatchingAny1 r => String -> ExprVar tp -> ValuePerm tp ->
+                Mb vars (ValuePerm tp) -> ImplM vars s r ps_any ps a
+implFailVarM f x p mb_p =
+  use implStatePPInfo >>>= \ppinfo ->
+  use implStateVars >>>= \ctx ->
+  findPermsContainingVar x >>>= \case
+    (Some distperms) ->
+      implFailM $ ImplVariableError 
+                    (ppImpl ppinfo x p mb_p) 
+                    f 
+                    (permPretty ppinfo x, x) 
+                    (permPretty ppinfo p, p)
+                    ctx 
+                    distperms
+
+  -- ImplVariableError 
+  --   :: Doc ann -> String 
+  --   -> ExprVar tp -> ValuePerm tp -> CruCtx vars 
+  --   -> Some DistPerms -> Mb vars (ValuePerm tp) 
+  --   -> ImplError
+
+
+
+-- | Emit debugging output using the current 'PPInfo' if the 'implStateDoTrace'
+-- flag is set
+implTraceM :: (PPInfo -> PP.Doc ann) -> ImplM vars s r ps ps String
+implTraceM f =
+  do do_trace <- use implStateDoTrace
+     doc <- uses implStatePPInfo f
+     let str = renderDoc doc
+     fn do_trace str (pure str)
+  where
+    fn True  = trace
+    fn False = const id
+
+
+instance ErrorPretty ImplError where
+  ppError (GeneralError doc) = renderDoc doc
+  ppError NoFrameInScopeError = 
+    "No LLVM frame in scope"
+  ppError ArrayStepError = 
+    "Error proving array permissions"
+  ppError MuUnfoldError =
+    "Tried to unfold a mu on the left after unfolding on the right"
+  ppError FunctionPermissionError =
+    "Could not find function permission"
+  ppError (PartialSubstitutionError caller doc) = renderDoc $
+    sep [ pretty ("Incomplete susbtitution in " ++ caller ++ " for: ")
+        , doc ]
+  ppError (LifetimeError EndLifetimeError) =
+    "implEndLifetimeM: lownedPermsToDistPerms"
+  ppError (LifetimeError ImplicationLifetimeError) =
+    "proveVarAtomicImpl: lownedPermsToDistPerms"
+  ppError (LifetimeError (LifetimeCurrentError doc)) = renderDoc $
+    pretty "Could not prove lifetime is current:" <+> doc
+  ppError (MemBlockError doc) = renderDoc $
+    pretty "Could not eliminate permission" <+> doc
+    -- permPretty pp (Perm_LLVMBlock bp)
+  ppError (EqualityProofError edoc mbedoc) = renderDoc $
+    sep [ pretty "proveEq" <> colon <+> pretty "Could not prove"
+        , edoc <+> pretty "=" <+> mbedoc]
+  ppError (InsufficientVariablesError doc) = renderDoc $
+    sep [PP.fillSep [PP.pretty
+          "Could not determine enough variables to prove permissions:",
+          doc]]
+  ppError (ExistentialError docx docp ) = renderDoc $
+    pretty "proveExVarImpl: existential variable" <+>
+    docx <+>
+    pretty "not resolved when trying to prove:" <> softline <>
+    docp
+  ppError (ImplVariableError doc f _ev _vp _ctx _dp) = renderDoc $
+    sep [ pretty f <> colon <+> pretty "Could not prove"
+        , doc ]
+
+
+$(mkNuMatching [t| forall a. EqPerm a |])
+$(mkNuMatching [t| forall ps a. NuMatching a => EqProofStep ps a |])
+$(mkNuMatching [t| forall ps a. NuMatching a => EqProof ps a |])
+$(mkNuMatching [t| forall ps_in ps_out. SimplImpl ps_in ps_out |])
+$(mkNuMatching [t| LifetimeErrorType |])
+$(mkNuMatching [t| ImplError |])
+$(mkNuMatching [t| forall ps_in ps_outs. PermImpl1 ps_in ps_outs |])
+$(mkNuMatching [t| forall r bs_pss. NuMatchingAny1 r => MbPermImpls r bs_pss |])
+$(mkNuMatching [t| forall r ps. NuMatchingAny1 r => PermImpl r ps |])
+$(mkNuMatching [t| forall ps_in ps_out. LocalPermImpl ps_in ps_out |])
+$(mkNuMatching [t| forall ps ps'. LocalImplRet ps ps' |])
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/ImplicationError.hs b/heapster-saw/src/Verifier/SAW/Heapster/ImplicationError.hs
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/JSONExport.hs b/heapster-saw/src/Verifier/SAW/Heapster/JSONExport.hs
new file mode 100644
index 0000000000..5e8103488b
--- /dev/null
+++ b/heapster-saw/src/Verifier/SAW/Heapster/JSONExport.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedLists, OverloadedStrings #-}
+{-# LANGUAGE ParallelListComp #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -Wno-orphans #-} -- hobbits instances for Value
+module Verifier.SAW.Heapster.JSONExport
+  (JsonExport, JsonExport1, ppToJson)
+  where
+
+import Data.Aeson ( ToJSON(toJSON), Value(..), object )
+import Data.Binding.Hobbits
+import Data.BitVector.Sized ( BV, asUnsigned )
+import Data.Kind (Type)
+import Data.Parameterized.BoolRepr ( BoolRepr )
+import Data.Parameterized.Context ( Assignment )
+import Data.Parameterized.Nonce (Nonce, indexValue)
+import Data.Parameterized.TraversableFC ( FoldableFC(toListFC) )
+import Data.Text (Text)
+import Data.Traversable (for)
+import Data.Type.RList ( mapToList )
+import GHC.Natural (Natural)
+import Lang.Crucible.FunctionHandle ( FnHandle )
+import Lang.Crucible.LLVM.Bytes ( Bytes )
+import Lang.Crucible.Types
+import qualified Language.Haskell.TH as TH
+import qualified Language.Haskell.TH.Datatype as TH
+import Verifier.SAW.Heapster.CruUtil ( CruCtx )
+import Verifier.SAW.Heapster.Implication
+import Verifier.SAW.Heapster.Permissions
+import Verifier.SAW.Name ( Ident )
+import What4.FunctionName ( FunctionName )
+
+instance NuMatching Value where
+    nuMatchingProof = unsafeMbTypeRepr
+
+instance Liftable Value where
+    mbLift = unClosed . mbLift . fmap unsafeClose
+
+-- | Uniformly export the algebraic datatype structure
+-- Heapster permissions.
+ppToJson :: JsonExport a => PPInfo -> a -> Value
+ppToJson ppi = let ?ppi = ppi in jsonExport
+
+-- | Class of types that can be uniformly exported as JSON
+-- using the Heapster pretty-printing information for names
+class JsonExport a where
+    jsonExport :: (?ppi::PPInfo) => a -> Value
+    default jsonExport :: ToJSON a => (?ppi::PPInfo) => a -> Value
+    jsonExport = toJSON
+
+instance JsonExport (Name (t :: CrucibleType)) where
+    jsonExport = toJSON . permPrettyString ?ppi
+
+instance JsonExport1 f => JsonExport (Assignment f x) where
+    jsonExport = toJSON . toListFC jsonExport1
+
+instance JsonExport1 f => JsonExport (RAssign f x) where
+    jsonExport = toJSON . mapToList jsonExport1
+
+
+instance JsonExport b => JsonExport (Mb (a :: RList CrucibleType) b) where
+    jsonExport mb = mbLift $ flip nuMultiWithElim1 mb $ \names body ->
+        let ?ppi = ppInfoAddExprNames "x" names ?ppi in
+        object [
+            ("args", jsonExport names),
+            ("body", jsonExport body)
+        ]
+
+instance JsonExport (Nonce a b) where
+    jsonExport = toJSON . indexValue
+
+instance JsonExport Bytes where
+    jsonExport = toJSON . show -- Show instance is pretty
+
+instance JsonExport Ident where
+    jsonExport = toJSON . show -- Show instance is pretty
+
+instance JsonExport FunctionName where
+    jsonExport = toJSON . show -- Show instance is pretty
+
+instance JsonExport (EqProof a b) where
+    jsonExport _ = object []
+
+instance JsonExport a => JsonExport (Maybe a) where
+    jsonExport = maybe Null jsonExport
+
+instance (JsonExport a, JsonExport b) => JsonExport (a,b) where
+    jsonExport (x,y) = toJSON (jsonExport x, jsonExport y)
+
+instance JsonExport a => JsonExport [a] where
+    jsonExport xs = toJSON (jsonExport <$> xs)
+
+instance JsonExport (BV n) where
+    jsonExport = toJSON . asUnsigned
+
+instance JsonExport (Proxy a) where
+    jsonExport _ = object []
+
+instance JsonExport ImplError where
+    jsonExport = toJSON . ppError
+
+-- Custom instance avoids the polymorphic field on the Done case
+instance JsonExport (PermImpl f ps) where
+    jsonExport (PermImpl_Done _eq) =
+        object [("tag", "PermImpl_Done")]
+    jsonExport (PermImpl_Step rs mb) =
+        object
+            [("tag", "PermImpl_Step"),
+             ("contents", Array
+                [jsonExport rs,
+                 jsonExport mb])]
+
+instance JsonExport Natural
+instance JsonExport Integer
+instance JsonExport Int
+instance JsonExport Bool
+instance JsonExport Text
+instance {-# OVERLAPPING #-} JsonExport String
+
+-- | 'JsonExport' lifted to work on types with higher kinds
+class JsonExport1 f where
+    jsonExport1 :: (?ppi::PPInfo) => f a -> Value
+    default jsonExport1 :: JsonExport (f a) => (?ppi::PPInfo) => f a -> Value
+    jsonExport1 = jsonExport
+
+instance JsonExport1 BaseTypeRepr
+instance JsonExport1 TypeRepr
+instance JsonExport1 (Name :: CrucibleType -> Type)
+instance JsonExport1 LOwnedPerm
+instance JsonExport1 PermExpr
+instance JsonExport1 ValuePerm
+instance JsonExport1 VarAndPerm
+instance JsonExport1 Proxy
+
+-- This code generates generic JSON generation instances for
+-- algebraic data types.
+--
+-- - All instances will generate an object.
+-- - The object will have a @tag@ field containing the name
+--   of the constructor used.
+-- - Record constructors will add each record field to the
+--   object using the field name
+-- - Normal constructors with fields will have a field called
+--   @contents@. If this constructor has more than one parameter
+--   the @contents@ field will have a list. Otherwise it will
+--   have a single element.
+let fields :: String -> TH.ConstructorVariant -> [TH.ExpQ] -> TH.ExpQ
+
+    -- Record constructor, use record field names as JSON field names
+    fields tag (TH.RecordConstructor fieldNames) xs =
+        TH.listE
+          $ [| ("tag", tag) |]
+          : [ [| (n, $x) |] | n <- TH.nameBase <$> fieldNames | x <- xs]
+
+    -- No fields, so just report the constructor tag
+    fields tag _ []  = [| [("tag", tag)] |]
+
+    -- One field, just report that field as @contents@
+    fields tag _ [x] = [| [("tag", tag), ("contents", $x)] |]
+
+    -- Multiple fields, report them as a list as @contents@
+    fields tag _ xs  = [| [("tag", tag), ("contents", Array $(TH.listE xs))] |]
+
+    clauses :: TH.DatatypeInfo -> [TH.ClauseQ]
+    clauses info =
+        [do fieldVars <- for [0..length (TH.constructorFields con)-1] $ \i ->
+                            TH.newName ("x" ++ show i)
+            TH.clause
+              [TH.conP (TH.constructorName con) (TH.varP <$> fieldVars)]
+              (TH.normalB [|
+                object
+                    $(fields
+                        (TH.nameBase (TH.constructorName con))
+                        (TH.constructorVariant con)
+                        [ [| jsonExport $(TH.varE v) |] | v <- fieldVars ]) |])
+              []
+        | con <- TH.datatypeCons info ]
+
+    generateJsonExport :: TH.Name -> TH.DecQ
+    generateJsonExport n =
+      do info <- TH.reifyDatatype n
+         let t = foldl TH.appT (TH.conT n)
+               $ zipWith (\c _ -> TH.varT (TH.mkName [c])) ['a'..]
+               $ TH.datatypeInstTypes info
+         TH.instanceD (TH.cxt []) [t|JsonExport $t|]
+           [TH.funD 'jsonExport (clauses info)]
+
+    typesNeeded :: [TH.Name]
+    typesNeeded =
+        [''AtomicPerm, ''BaseTypeRepr, ''BoolRepr, ''BVFactor, ''BVProp,
+        ''BVRange, ''CruCtx, ''FloatInfoRepr, ''FloatPrecisionRepr,
+        ''FnHandle, ''FunPerm, ''LLVMArrayBorrow, ''LLVMArrayField,
+        ''LLVMArrayIndex, ''LLVMArrayPerm, ''LLVMBlockPerm, ''LLVMFieldPerm,
+        ''LLVMFieldShape, ''LOwnedPerm, ''NamedPermName, ''NamedShape,
+        ''NamedShapeBody, ''NameReachConstr, ''NameSortRepr, ''NatRepr,
+        ''PermExpr, ''PermOffset, ''StringInfoRepr, ''SymbolRepr, ''TypeRepr,
+        ''ValuePerm, ''RWModality, ''PermImpl1, ''Member, ''SimplImpl,
+        ''VarAndPerm, ''LocalPermImpl, ''LifetimeFunctor, ''NamedPerm,
+        ''RecPerm, ''OpaquePerm, ''DefinedPerm, ''ReachMethods, ''MbPermImpls
+        ]
+
+ in traverse generateJsonExport typesNeeded
+
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/NamedMb.hs b/heapster-saw/src/Verifier/SAW/Heapster/NamedMb.hs
new file mode 100644
index 0000000000..ca7f1ed131
--- /dev/null
+++ b/heapster-saw/src/Verifier/SAW/Heapster/NamedMb.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeOperators #-}
+module Verifier.SAW.Heapster.NamedMb where
+
+import Data.Binding.Hobbits
+import Data.Binding.Hobbits.MonadBind
+import Data.Type.RList
+import Control.Lens
+
+newtype StringF a = StringF { unStringF :: String }
+
+type Binding' c = Mb' (RNil :> c)
+
+data Mb' ctx a = Mb'
+  { _mbNames :: RAssign StringF ctx
+  , _mbBinding :: Mb ctx a
+  }
+  deriving Functor
+
+mbBinding :: Lens (Mb' ctx a) (Mb' ctx b) (Mb ctx a) (Mb ctx b)
+mbBinding f x = Mb' (_mbNames x) <$> f (_mbBinding x)
+
+nuMulti' :: RAssign StringF ctx -> (RAssign Name ctx -> b) -> Mb' ctx b
+nuMulti' tps f = Mb'
+  { _mbNames = tps
+  , _mbBinding = nuMulti (mapRAssign (const Proxy) tps) f
+  }
+
+nuMultiWithElim1' :: (RAssign Name ctx -> arg -> b) -> Mb' ctx arg -> Mb' ctx b
+nuMultiWithElim1' k = over mbBinding (nuMultiWithElim1 k)
+
+
+strongMbM' :: MonadStrongBind m => Mb' ctx (m a) -> m (Mb' ctx a)
+strongMbM' = traverseOf mbBinding strongMbM
+
+mbM' :: (MonadBind m, NuMatching a) => Mb' ctx (m a) -> m (Mb' ctx a)
+mbM' = traverseOf mbBinding mbM
+
+mbSwap' :: RAssign Proxy ctx -> Mb' ctx' (Mb' ctx a) -> Mb' ctx (Mb' ctx' a)
+mbSwap' p (Mb' names' body') =
+    Mb'
+    { _mbNames = mbLift (_mbNames <$> body')
+    , _mbBinding = Mb' names' <$> mbSwap p (_mbBinding <$> body')
+    }
+
+mbSink :: RAssign Proxy ctx -> Mb ctx' (Mb' ctx a) -> Mb' ctx (Mb ctx' a)
+mbSink p m =
+    Mb'
+    { _mbNames = mbLift (_mbNames <$> m)
+    , _mbBinding = mbSwap p (_mbBinding <$> m)
+    }
+
+mbLift' :: Liftable a => Mb' ctx a -> a
+mbLift' = views mbBinding mbLift
+
+elimEmptyMb' :: Mb' RNil a -> a
+elimEmptyMb' = views mbBinding elimEmptyMb
+
+emptyMb' :: a -> Mb' RNil a
+emptyMb' = Mb' MNil . emptyMb
+
+mkNuMatching [t| forall a. StringF a |]
+instance NuMatchingAny1 StringF where
+    nuMatchingAny1Proof = nuMatchingProof
+
+instance Liftable (StringF a) where
+    mbLift (mbMatch -> [nuMP| StringF x |]) = StringF (mbLift x)
+
+instance LiftableAny1 StringF where
+    mbLiftAny1 = mbLift
+
+mkNuMatching [t| forall ctx a. NuMatching a => Mb' ctx a |]
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 7e0c779ac5..abf0b475ca 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -79,6 +79,7 @@ import Lang.Crucible.LLVM.Bytes
 import Lang.Crucible.CFG.Core
 import Verifier.SAW.Term.Functor (Ident)
 import Verifier.SAW.OpenTerm
+import Verifier.SAW.Heapster.NamedMb
 
 import Verifier.SAW.Heapster.CruUtil
 
@@ -137,8 +138,6 @@ foldMapWithDefault comb def f l = foldr1WithDefault comb def $ map f l
 -- * Pretty-printing
 ----------------------------------------------------------------------
 
-newtype StringF a = StringF { unStringF :: String }
-
 -- | Convert a type to a base name for printing variables of that type
 typeBaseName :: TypeRepr a -> String
 typeBaseName UnitRepr = "u"
@@ -175,16 +174,24 @@ emptyPPInfo = PPInfo NameMap.empty Map.empty
 
 -- | Add an expression variable to a 'PPInfo' with the given base name
 ppInfoAddExprName :: String -> ExprVar a -> PPInfo -> PPInfo
-ppInfoAddExprName base _ _
+ppInfoAddExprName base x ppi =
+  let (ppi', str) = ppInfoAllocateName base ppi in
+  ppInfoApplyName x str ppi'
+
+ppInfoApplyName :: Name (x :: CrucibleType) -> String -> PPInfo -> PPInfo
+ppInfoApplyName x str ppi =
+  ppi { ppExprNames = NameMap.insert x (StringF str) (ppExprNames ppi) }
+
+ppInfoAllocateName :: String -> PPInfo -> (PPInfo, String)
+ppInfoAllocateName base _
   | length base == 0 || isDigit (last base) =
     error ("ppInfoAddExprName: invalid base name: " ++ base)
-ppInfoAddExprName base x (PPInfo { .. }) =
+ppInfoAllocateName base ppi =
   let (i',str) =
-        case Map.lookup base ppBaseNextInt of
+        case Map.lookup base (ppBaseNextInt ppi) of
           Just i -> (i+1, base ++ show i)
           Nothing -> (1, base) in
-  PPInfo { ppExprNames = NameMap.insert x (StringF str) ppExprNames,
-           ppBaseNextInt = Map.insert base i' ppBaseNextInt }
+  (ppi { ppBaseNextInt = Map.insert base i' (ppBaseNextInt ppi) }, str)
 
 -- | Add a sequence of variables to a 'PPInfo' with the given base name
 ppInfoAddExprNames :: String -> RAssign Name (tps :: RList CrucibleType) ->
@@ -193,12 +200,33 @@ ppInfoAddExprNames _ MNil info = info
 ppInfoAddExprNames base (ns :>: n) info =
   ppInfoAddExprNames base ns $ ppInfoAddExprName base n info
 
+-- |
+ppInfoAllocateExprNames ::
+  String {- ^ base name -} ->
+  RAssign pxy (tps :: RList CrucibleType) ->
+  PPInfo ->
+  (PPInfo, RAssign StringF tps)
+ppInfoAllocateExprNames _ MNil info = (info, MNil)
+ppInfoAllocateExprNames base (ns :>: _) ppi =
+  case ppInfoAllocateName base ppi of
+    (ppi1, str) ->
+      case ppInfoAllocateExprNames base ns ppi1 of
+        (ppi2, ns') -> (ppi2, ns' :>: StringF str)
+
 -- | Add a sequence of variables to a 'PPInfo' using their 'typeBaseName's
 ppInfoAddTypedExprNames :: CruCtx tps -> RAssign Name tps -> PPInfo -> PPInfo
 ppInfoAddTypedExprNames _ MNil info = info
 ppInfoAddTypedExprNames (CruCtxCons tps tp) (ns :>: n) info =
   ppInfoAddTypedExprNames tps ns $ ppInfoAddExprName (typeBaseName tp) n info
 
+ppInfoApplyAllocation ::
+  RAssign Name (tps :: RList CrucibleType) ->
+  RAssign StringF tps ->
+  PPInfo ->
+  PPInfo
+ppInfoApplyAllocation MNil MNil ppi = ppi
+ppInfoApplyAllocation (ns :>: n) (ss :>: StringF s) ppi =
+  ppInfoApplyAllocation ns ss (ppInfoApplyName n s ppi)
 
 type PermPPM = Reader PPInfo
 
@@ -313,15 +341,25 @@ instance PermPrettyF VarAndType where
 
 
 permPrettyExprMb :: PermPretty a =>
-                    (RAssign (Constant (Doc ann)) ctx -> PermPPM (Doc ann) -> PermPPM (Doc ann)) ->
-                    Mb (ctx :: RList CrucibleType) a -> PermPPM (Doc ann)
+  (RAssign (Constant (Doc ann)) ctx -> PermPPM (Doc ann) -> PermPPM (Doc ann)) ->
+  Mb (ctx :: RList CrucibleType) a -> PermPPM (Doc ann)
 permPrettyExprMb f mb =
   fmap mbLift $ strongMbM $ flip nuMultiWithElim1 mb $ \ns a ->
-  local (ppInfoAddExprNames "z" ns) $
+  local (ppInfoAddExprNames "x" ns) $
+  do docs <- traverseRAssign (\n -> Constant <$> permPrettyM n) ns
+     f docs $ permPrettyM a
+
+permPrettyExprMbTyped :: PermPretty a =>
+  CruCtx ctx ->
+  (RAssign (Constant (Doc ann)) ctx -> PermPPM (Doc ann) -> PermPPM (Doc ann)) ->
+  Mb (ctx :: RList CrucibleType) a -> PermPPM (Doc ann)
+permPrettyExprMbTyped ctx f mb =
+  fmap mbLift $ strongMbM $ flip nuMultiWithElim1 mb $ \ns a ->
+  local (ppInfoAddTypedExprNames ctx ns) $
   do docs <- traverseRAssign (\n -> Constant <$> permPrettyM n) ns
      f docs $ permPrettyM a
 
-instance PermPretty a => PermPretty (Mb (ctx :: RList CrucibleType) a) where
+instance (PermPretty a) => PermPretty (Mb (ctx :: RList CrucibleType) a) where
   permPrettyM =
     permPrettyExprMb $ \docs ppm ->
     (\pp -> PP.group (ppEncList True (RL.toList docs) <>
@@ -863,7 +901,7 @@ instance PermPretty (PermExpr a) where
        pp2 <- permPrettyM sh2
        return $ nest 2 $ sep [pp1 <+> pretty "orsh", pp2]
   permPrettyM (PExpr_ExShape mb_sh) =
-    flip permPrettyExprMb mb_sh $ \(_ :>: Constant pp_n) ppm ->
+    flip (permPrettyExprMbTyped (CruCtxNil `CruCtxCons` knownRepr)) mb_sh $ \(_ :>: Constant pp_n) ppm ->
     do pp <- ppm
        return $ nest 2 $ sep [pretty "exsh" <+> pp_n <> dot, pp]
   permPrettyM (PExpr_ValPerm p) = permPrettyM p
@@ -2564,7 +2602,7 @@ instance PermPretty (ValuePerm a) where
     (\pp1 pp2 -> hang 2 (pp1 <> softline <> pretty "or" <+> pp2))
     <$> permPrettyM p1 <*> permPrettyM p2
   permPrettyM (ValPerm_Exists mb_p) =
-    flip permPrettyExprMb mb_p $ \(_ :>: Constant pp_n) ppm ->
+    flip (permPrettyExprMbTyped (CruCtxNil `CruCtxCons` knownRepr)) mb_p $ \(_ :>: Constant pp_n) ppm ->
     (\pp -> hang 2 (pretty "exists" <+> pp_n <> dot <+> pp)) <$> ppm
   permPrettyM (ValPerm_Named n args off) =
     do n_pp <- permPrettyM n
@@ -2806,8 +2844,8 @@ $(mkNuMatching [t| forall ps. LifetimeCurrentPerms ps |])
 instance NuMatchingAny1 LOwnedPerm where
   nuMatchingAny1Proof = nuMatchingProof
 
-instance NuMatchingAny1 DistPerms where
-  nuMatchingAny1Proof = nuMatchingProof
+-- instance NuMatchingAny1 DistPerms where
+--   nuMatchingAny1Proof = nuMatchingProof
 
 instance Liftable RWModality where
   mbLift mb_rw = case mbMatch mb_rw of
@@ -4932,6 +4970,23 @@ genSubstMb ::
   s ctx' -> Mb ctx' (Mb ctx a) -> m (Mb ctx a)
 genSubstMb p s mbmb = mbM (fmap (genSubst s) (mbSwap p mbmb))
 
+
+instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx), Substable s a m, NuMatching a) => Substable s (Mb' ctx a) m where
+   genSubst = genSubstMb' given
+
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Mb' RNil a) m where
+   genSubst = genSubstMb' RL.typeCtxProxies
+
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Binding' c a) m where
+   genSubst = genSubstMb' RL.typeCtxProxies
+
+genSubstMb' ::
+  Substable s a m =>
+  NuMatching a =>
+  RAssign Proxy ctx ->
+  s ctx' -> Mb ctx' (Mb' ctx a) -> m (Mb' ctx a)
+genSubstMb' p s mbmb = mbM' (fmap (genSubst s) (mbSink p mbmb))
+
 instance SubstVar s m => Substable s (Member ctx a) m where
   genSubst _ mb_memb = return $ mbLift mb_memb
 
@@ -4941,6 +4996,10 @@ instance (NuMatchingAny1 f, Substable1 s f m) =>
     [nuMP| MNil |] -> return MNil
     [nuMP| xs :>: x |] -> (:>:) <$> genSubst s xs <*> genSubst1 s x
 
+instance (NuMatchingAny1 f, Substable1 s f m) =>
+         Substable1 s (RAssign f) m where
+  genSubst1 = genSubst
+
 instance (NuMatchingAny1 f, Substable1 s f m) =>
          Substable s (Assignment f ctx) m where
   genSubst s mb_assign =
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index d6a096ec1c..622586c624 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -77,6 +77,7 @@ import Verifier.SAW.Heapster.CruUtil
 import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.Implication
 import Verifier.SAW.Heapster.TypedCrucible
+import Verifier.SAW.Heapster.NamedMb
 
 import GHC.Stack
 import Debug.Trace
@@ -2644,10 +2645,10 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        let fromJustOrError (Just x) = x
            fromJustOrError Nothing = error "translateSimplImpl: SImpl_MapLifetime"
            ps_in'_vars =
-             RL.map (translateVar . getCompose) $ mbRAssign $ 
+             RL.map (translateVar . getCompose) $ mbRAssign $
              fmap (fromJustOrError . lownedPermsVars) ps_in'
            ps_out_vars =
-             RL.map (translateVar . getCompose) $ mbRAssign $ 
+             RL.map (translateVar . getCompose) $ mbRAssign $
              fmap (fromJustOrError . lownedPermsVars) ps_out
        impl_in_tm <-
          translateCurryLocalPermImpl "Error mapping lifetime input perms:" impl_in
@@ -2789,7 +2790,6 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            m
 
     | otherwise -> fail "translateSimplImpl: SImpl_IntroLLVMBlockNamed, unknown named shape"
-
   -- Elim for a recursive named shape applies the unfold function to the
   -- translations of the arguments plus the translations of the proofs of the
   -- permissions
@@ -3118,7 +3118,8 @@ translatePermImpl1 :: ImplTranslateF r ext blocks tops ret =>
 translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impls) of
   -- A failure translates to a call to the catch handler, which is the most recent
   -- Impl1_Catch, if one exists, or the SAW errorM function otherwise
-  ([nuMP| Impl1_Fail str |], _) -> pitmFail $ mbLift str
+  ([nuMP| Impl1_Fail err |], _) ->
+    tell ([mbLift (fmap ppError err)],HasFailures) >> mzero
 
   ([nuMP| Impl1_Catch |],
    [nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) ->
@@ -3798,7 +3799,7 @@ translateCallEntry nm entry_trans mb_tops_args mb_ghosts =
          -- If not, continue by translating entry, setting the variable
          -- permission map to empty (as in the beginning of a block)
          clearVarPermsM $ translate $
-         fmap (\s -> varSubst s $ typedEntryBody entry) mb_s
+         fmap (\s -> varSubst s $ _mbBinding $ typedEntryBody entry) mb_s
 
 
 instance PermCheckExtC ext =>
@@ -4084,7 +4085,7 @@ instance PermCheckExtC ext =>
   translate mb_x = case mbMatch mb_x of
     [nuMP| TypedImplStmt impl_seq |] -> translate impl_seq
     [nuMP| TypedConsStmt loc stmt pxys mb_seq |] ->
-      translateStmt (mbLift loc) stmt (translate $ mbCombine (mbLift pxys) mb_seq)
+      translateStmt (mbLift loc) stmt (translate $ mbCombine (mbLift pxys) (_mbBinding <$> mb_seq))
     [nuMP| TypedTermStmt _ term_stmt |] -> translate term_stmt
 
 instance PermCheckExtC ext =>
@@ -4214,7 +4215,7 @@ translateEntryBody mapTrans entry =
   lambdaPermCtx (typedEntryPermsIn entry) $ \pctx ->
   do retType <- translateEntryRetType entry
      impTransM (RL.members pctx) pctx mapTrans retType $ translate $
-       typedEntryBody entry
+       _mbBinding $ typedEntryBody entry
 
 -- | Translate all the entrypoints in a 'TypedBlockMap' that correspond to
 -- letrec-bound functions to SAW core functions as in 'translateEntryBody'
@@ -4352,14 +4353,30 @@ someCFGAndPermPtrPerm (SomeCFGAndPerm _ _ _ fun_perm) =
 tcTranslateCFGTupleFun ::
   HasPtrWidth w =>
   PermEnv -> EndianForm -> [SomeCFGAndPerm LLVM] ->
-  (OpenTerm, OpenTerm)
+  (OpenTerm, [SomeTypedCFG LLVM], OpenTerm)
 tcTranslateCFGTupleFun env endianness cfgs_and_perms =
-  let lrts = map (someCFGAndPermLRT env) cfgs_and_perms in
-  let lrts_tm =
+  let lrts = map (someCFGAndPermLRT env) cfgs_and_perms
+
+      lrts_tm =
         foldr (\lrt lrts' -> ctorOpenTerm "Prelude.LRT_Cons" [lrt,lrts'])
         (ctorOpenTerm "Prelude.LRT_Nil" [])
-        lrts in
-  (lrts_tm ,) $
+        lrts
+
+      fakeEnv = withKnownNat ?ptrWidth $
+                permEnvAddGlobalSyms env $
+                  map (\cfg_and_perm ->
+                        PermEnvGlobalEntry
+                          (someCFGAndPermSym cfg_and_perm)
+                          (someCFGAndPermPtrPerm cfg_and_perm)
+                          [error "TODO: put something here"])
+                    cfgs_and_perms
+
+      tcfgs = map (\cfg_and_perms ->
+                      case cfg_and_perms of
+                        SomeCFGAndPerm _ _ cfg fun_perm ->
+                          SomeTypedCFG $ tcCFG ?ptrWidth fakeEnv endianness fun_perm cfg) cfgs_and_perms
+  in
+  (lrts_tm , tcfgs, ) $
   lambdaOpenTermMulti (zip
                        (map (pack . someCFGAndPermToName) cfgs_and_perms)
                        (map (applyOpenTerm
@@ -4409,9 +4426,9 @@ tcTranslateAddCFGs ::
   HasPtrWidth w =>
   SharedContext -> ModuleName ->
   PermEnv -> EndianForm -> [SomeCFGAndPerm LLVM] ->
-  IO PermEnv
+  IO (PermEnv, [SomeTypedCFG LLVM])
 tcTranslateAddCFGs sc mod_name env endianness cfgs_and_perms =
-  do let (lrts, tup_fun) =
+  do let (lrts, tcfgs, tup_fun) =
            tcTranslateCFGTupleFun env endianness cfgs_and_perms
      let tup_fun_ident =
            mkSafeIdent mod_name (someCFGAndPermToName (head cfgs_and_perms)
@@ -4420,7 +4437,7 @@ tcTranslateAddCFGs sc mod_name env endianness cfgs_and_perms =
        applyOpenTerm (globalOpenTerm "Prelude.lrtTupleType") lrts
      tup_fun_tm <- completeOpenTerm sc $
        applyOpenTermMulti (globalOpenTerm "Prelude.multiFixM") [lrts, tup_fun]
-     scInsertDef sc mod_name tup_fun_ident tup_fun_tp tup_fun_tm 
+     scInsertDef sc mod_name tup_fun_ident tup_fun_tp tup_fun_tm
      new_entries <-
        zipWithM
        (\cfg_and_perm i ->
@@ -4436,7 +4453,7 @@ tcTranslateAddCFGs sc mod_name env endianness cfgs_and_perms =
               (someCFGAndPermPtrPerm cfg_and_perm)
               [globalOpenTerm ident])
        cfgs_and_perms [0 ..]
-     return $ permEnvAddGlobalSyms env new_entries
+     return (permEnvAddGlobalSyms env new_entries, tcfgs)
 
 
 ----------------------------------------------------------------------
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index 805c890fec..a46ddc6652 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -50,7 +50,6 @@ import Prettyprinter as PP
 
 import qualified Data.Type.RList as RL
 import Data.Binding.Hobbits
-import Data.Binding.Hobbits.MonadBind
 import Data.Binding.Hobbits.NameSet (NameSet, SomeName(..), SomeRAssign(..),
                                      namesListToNames, namesToNamesList,
                                      nameSetIsSubsetOf)
@@ -80,6 +79,7 @@ import Verifier.SAW.Heapster.Implication
 import Verifier.SAW.Heapster.NamePropagation
 import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.Widening
+import Verifier.SAW.Heapster.NamedMb
 
 import Debug.Trace
 
@@ -368,7 +368,6 @@ instance Closable (TypedCallSiteID blocks args vars) where
 instance Liftable (TypedCallSiteID blocks args vars) where
   mbLift = unClosed . mbLift . fmap toClosed
 
-
 ----------------------------------------------------------------------
 -- * Typed Crucible Statements
 ----------------------------------------------------------------------
@@ -472,7 +471,7 @@ data TypedLLVMStmt ret ps_in ps_out where
   -- Type:
   -- > ps, x:ptr((rw,0) |-> p), cur_ps
   -- > -o ps, x:ptr((rw,0) |-> eq(ret)), ret:p, cur_ps
-  TypedLLVMLoad :: 
+  TypedLLVMLoad ::
     (HasPtrWidth w, 1 <= sz, KnownNat sz) =>
     !(TypedReg (LLVMPointerType w)) ->
     !(LLVMFieldPerm w sz) ->
@@ -544,7 +543,7 @@ data TypedLLVMStmt ret ps_in ps_out where
   -- referred to by a function pointer, assuming we know it has one:
   --
   -- Type: @x:llvm_funptr(p) -o ret:p@
-  TypedLLVMLoadHandle :: 
+  TypedLLVMLoadHandle ::
     HasPtrWidth w =>
     !(TypedReg (LLVMPointerType w)) ->
     !(TypeRepr (FunctionHandleType cargs ret)) ->
@@ -761,7 +760,7 @@ data TypedStmtSeq ext blocks tops ret ps_in where
   TypedConsStmt :: !ProgramLoc ->
                    !(TypedStmt ext rets ps_in ps_next) ->
                    !(RAssign Proxy rets) ->
-                   !(Mb rets (TypedStmtSeq ext blocks tops ret ps_next)) ->
+                   !(Mb' rets (TypedStmtSeq ext blocks tops ret ps_next)) ->
                    TypedStmtSeq ext blocks tops ret ps_in
 
   -- | Typed version of 'TermStmt', which terminates the current block
@@ -1210,11 +1209,12 @@ data TypedEntry phase ext blocks tops ret args ghosts =
     typedEntryPermsOut :: !(MbValuePerms (tops :> ret)),
     -- | The type-checked body of the entrypoint
     typedEntryBody :: !(TransData phase
-                        (Mb ((tops :++: args) :++: ghosts)
+                        (Mb' ((tops :++: args) :++: ghosts)
                          (TypedStmtSeq ext blocks tops ret
                           ((tops :++: args) :++: ghosts))))
   }
 
+
 -- | Test if an entrypoint has in-degree greater than 1
 typedEntryHasMultiInDegree :: TypedEntry phase ext blocks tops ret args ghosts ->
                               Bool
@@ -1239,11 +1239,12 @@ completeTypedEntry _ = Nothing
 
 -- | Build an entrypoint from a call site, using that call site's permissions as
 -- the entyrpoint input permissions
-singleCallSiteEntry :: TypedCallSiteID blocks args vars ->
-                       CruCtx tops -> CruCtx args -> TypeRepr ret ->
-                       MbValuePerms ((tops :++: args) :++: vars) ->
-                       MbValuePerms (tops :> ret) ->
-                       TypedEntry TCPhase ext blocks tops ret args vars
+singleCallSiteEntry ::
+  TypedCallSiteID blocks args vars ->
+  CruCtx tops -> CruCtx args -> TypeRepr ret ->
+  MbValuePerms ((tops :++: args) :++: vars) ->
+  MbValuePerms (tops :> ret) ->
+  TypedEntry TCPhase ext blocks tops ret args vars
 singleCallSiteEntry siteID tops args ret perms_in perms_out =
   TypedEntry
   {
@@ -1640,6 +1641,10 @@ data TypedCFG
              , tpcfgEntryID :: !(TypedEntryID blocks inits)
              }
 
+data SomeTypedCFG ext where
+  SomeTypedCFG :: PermCheckExtC ext =>
+    TypedCFG ext blocks ghosts inits ret -> SomeTypedCFG ext
+
 -- | Get the input permissions for a 'CFG'
 tpcfgInputPerms :: TypedCFG ext blocks ghosts inits ret ->
                    MbValuePerms (ghosts :++: inits)
@@ -1934,26 +1939,73 @@ runPermCheckM ::
    DistPerms ((tops :++: args) :++: ghosts) ->
    PermCheckM ext cblocks blocks tops ret () ps_out r ((tops :++: args)
                                                        :++: ghosts) ()) ->
-  TopPermCheckM ext cblocks blocks tops ret (Mb ((tops :++: args) :++: ghosts) r)
+  TopPermCheckM ext cblocks blocks tops ret (Mb' ((tops :++: args) :++: ghosts) r)
 runPermCheckM names entryID args ghosts mb_perms_in m =
   get >>= \(TopPermCheckState {..}) ->
   let args_prxs = cruCtxProxies args
-      ghosts_prxs = cruCtxProxies ghosts in
-  liftInnerToTopM $ strongMbM $
-  flip nuMultiWithElim1 (mbValuePermsToDistPerms mb_perms_in) $ \ns perms_in ->
+      ghosts_prxs = cruCtxProxies ghosts
+      (arg_names, local_names) = initialNames args names
+      (dbgs, ppi) = flip runState emptyPPInfo $
+          do x <- state (allocateDebugNames' (Just "top") (noNames' stTopCtx) stTopCtx)
+             y <- state (allocateDebugNames' (Just "local") arg_names args)
+             z <- state (allocateDebugNames' (Just "ghost") (noNames' ghosts) ghosts)
+             pure (x `rappend` y `rappend` z)
+    in
+  liftInnerToTopM $ strongMbM' $
+  flip nuMultiWithElim1' (Mb' dbgs (mbValuePermsToDistPerms mb_perms_in)) $ \ns perms_in ->
   let (tops_args, ghosts_ns) = RL.split Proxy ghosts_prxs ns
       (tops_ns, args_ns) = RL.split Proxy args_prxs tops_args
-      (arg_names, local_names) = initialNames args names
-      st = emptyPermCheckState (distPermSet perms_in) tops_ns entryID local_names in
-  
+      st1 = emptyPermCheckState (distPermSet perms_in) tops_ns entryID local_names
+      st = st1 { stPPInfo = ppi } in
   let go x = runGenStateContT x st (\_ () -> pure ()) in
   go $
-  setVarTypes (Just "top") (noNames' stTopCtx) tops_ns stTopCtx >>>
-  setVarTypes (Just "local") arg_names args_ns args >>>
-  setVarTypes (Just "ghost") (noNames' ghosts) ghosts_ns ghosts >>>
+  setVarTypes' tops_ns stTopCtx >>>
+  setVarTypes' args_ns args >>>
+  setVarTypes' ghosts_ns ghosts >>>
+  modify (\s->s{ stPPInfo = ppInfoApplyAllocation ns dbgs (stPPInfo st)}) >>>
   setInputExtState knownRepr ghosts ghosts_ns >>>
   m tops_ns args_ns ghosts_ns perms_in
 
+{-
+explore ::
+  forall tops args ghosts ext blocks cblocks ret ps r1 r2.
+  KnownRepr ExtRepr ext =>
+  [Maybe String] ->
+      TypedEntryID blocks args ->
+      CruCtx tops ->
+      CruCtx args ->
+      CruCtx ghosts ->
+      MbValuePerms ((tops :++: args) :++: ghosts) ->
+      
+    (RAssign ExprVar tops -> RAssign ExprVar args -> RAssign ExprVar ghosts ->
+      DistPerms ((tops :++: args) :++: ghosts) ->
+      PermCheckM ext cblocks blocks tops ret r1 ps r2 ((tops :++: args)
+                                                          :++: ghosts) ()) ->
+
+      PermCheckM ext cblocks blocks tops ret r1 ps r2 ps ()
+explore names entryID topCtx argCtx ghostCtx mb_perms_in m =
+  let args_prxs = cruCtxProxies argCtx
+      ghosts_prxs = cruCtxProxies ghostCtx
+      (arg_names, local_names) = initialNames argCtx names in
+
+  allocateDebugNames (Just "top") (noNames' topCtx) topCtx >>>= \topDbgs ->
+  allocateDebugNames (Just "local") arg_names argCtx >>>= \argDbgs ->
+  allocateDebugNames (Just "ghost") (noNames' ghostCtx) ghostCtx >>>= \ghostDbgs ->
+  gopenBinding (fmap _ . strongMbM) (mbValuePermsToDistPerms mb_perms_in) >>>= \(ns, perms_in) ->
+  let (tops_args, ghosts_ns) = RL.split Proxy ghosts_prxs ns
+      (tops_ns, args_ns) = RL.split Proxy args_prxs tops_args
+      st :: PermCheckState ext blocks tops ret ((tops :++: args) :++: ghosts)
+      st = emptyPermCheckState (distPermSet perms_in) tops_ns entryID local_names in
+  
+  setVarTypes' tops_ns topCtx >>>
+  modify (\s->s{ stPPInfo = ppInfoApplyAllocation tops_ns topDbgs (stPPInfo st)}) >>>
+  modify (\s->s{ stPPInfo = ppInfoApplyAllocation args_ns argDbgs (stPPInfo st)}) >>>
+  modify (\s->s{ stPPInfo = ppInfoApplyAllocation ghosts_ns ghostDbgs (stPPInfo st)}) >>>
+  setInputExtState knownRepr ghostCtx ghosts_ns >>>
+  m tops_ns args_ns ghosts_ns perms_in
+
+  -}
+
 rassignLen :: RAssign f x -> Int
 rassignLen = go 0
   where
@@ -2121,11 +2173,8 @@ getAtomicOrWordLLVMPerms r =
                                                recombinePerm x p) >>>
       pure (Left e_word)
     _ ->
-      stmtFailM (\i ->
-                  sep [pretty "getAtomicOrWordLLVMPerms:",
-                       pretty "Needed atomic permissions for" <+> permPretty i r,
-                       pretty "but found" <+>
-                       permPretty i p])
+      permGetPPInfo >>>= \ppinfo ->
+        stmtFailM $ AtomicPermError (permPretty ppinfo r) (permPretty ppinfo p)
 
 
 -- | Like 'getAtomicOrWordLLVMPerms', but fail if an equality permission to a
@@ -2141,11 +2190,11 @@ getAtomicLLVMPerms r =
   case eith of
     Right ps -> pure ps
     Left e ->
-      stmtFailM (\i ->
-                  sep [pretty "getAtomicLLVMPerms:",
-                       pretty "Needed atomic permissions for" <+> permPretty i r,
-                       pretty "but found" <+>
-                       permPretty i (ValPerm_Eq $ PExpr_LLVMWord e)])
+      permGetPPInfo >>>= \ppinfo ->
+        stmtFailM $ AtomicPermError 
+                      (permPretty ppinfo r) 
+                      (permPretty ppinfo (ValPerm_Eq $ PExpr_LLVMWord e))
+
 
 data SomeExprVarFrame where
   SomeExprVarFrame ::
@@ -2231,31 +2280,64 @@ setVarTypes str (ds :>: Constant d) (ns :>: n) (CruCtxCons ts t) =
   do setVarTypes str ds ns ts
      setVarType str d n t
 
--- | Get the current 'PPInfo'
-permGetPPInfo :: PermCheckM ext cblocks blocks tops ret r ps r ps PPInfo
-permGetPPInfo = gets stPPInfo
+-- | Remember the type of a free variable, and ensure that it has a permission
+setVarType' ::
+  ExprVar a -> -- ^ The Hobbits variable itself
+  TypeRepr a -> -- ^ The type of the variable
+  PermCheckM ext cblocks blocks tops ret r ps r ps ()
+setVarType' x tp =
+  modify $ \st ->
+  st { stCurPerms = initVarPerm x (stCurPerms st),
+       stVarTypes = NameMap.insert x tp (stVarTypes st) }
 
--- | Get the current prefix string to give context to error messages
-getErrorPrefix :: PermCheckM ext cblocks blocks tops ret r ps r ps (Doc ())
-getErrorPrefix = gets (fromMaybe emptyDoc . stErrPrefix)
+-- | Remember the types of a sequence of free variables
+setVarTypes' ::
+  RAssign Name tps ->
+  CruCtx tps ->
+  PermCheckM ext cblocks blocks tops ret r ps r ps ()
+setVarTypes' MNil CruCtxNil = pure ()
+setVarTypes' (ns :>: n) (CruCtxCons ts t) =
+  do setVarTypes' ns ts
+     setVarType' n t
 
--- | Emit debugging output using the current 'PPInfo'
-stmtTraceM :: (PPInfo -> Doc ()) ->
-              PermCheckM ext cblocks blocks tops ret r ps r ps String
-stmtTraceM f =
-  do doc <- f <$> permGetPPInfo
-     let str = renderDoc doc
-     trace str (pure str)
+allocateDebugNames ::
+  Maybe String -> -- ^ The bsae name of the variable (e.g., "top", "arg", etc.)
+  RAssign (Constant (Maybe String)) tps ->
+  CruCtx tps ->
+  PermCheckM ext cblocks blocks tops ret r ps r ps
+    (RAssign StringF tps)
+allocateDebugNames _ MNil _ = pure MNil
+allocateDebugNames base (ds :>: Constant dbg) (CruCtxCons ts tp) =
+  do outs <- allocateDebugNames base ds ts
+     out <- state $ \st ->
+              case ppInfoAllocateName str (stPPInfo st) of
+              (ppi, str') -> (str', st { stPPInfo = ppi })
+     pure (outs :>: StringF out)
+  where
+    str =
+      case (base,dbg) of
+        (_,Just d) -> "C[" ++ d ++ "]"
+        (Just b,_) -> b ++ "_" ++ typeBaseName tp
+        (Nothing,Nothing) -> typeBaseName tp
 
--- | Failure in the statement permission-checking monad
-stmtFailM :: (PPInfo -> Doc ()) -> PermCheckM ext cblocks blocks tops ret r1 ps1
-             (TypedStmtSeq ext blocks tops ret ps2) ps2 a
-stmtFailM msg =
-  getErrorPrefix >>>= \err_prefix ->
-  stmtTraceM (\i -> err_prefix <> line <>
-                    pretty "Type-checking failure:" <> softline <> msg i) >>>= \str ->
-  gabortM (return $ TypedImplStmt $ AnnotPermImpl str $
-           PermImpl_Step (Impl1_Fail "") MbPermImpls_Nil)
+allocateDebugNames' ::
+  Maybe String -> -- ^ The bsae name of the variable (e.g., "top", "arg", etc.)
+  RAssign (Constant (Maybe String)) tps ->
+  CruCtx tps ->
+  PPInfo ->
+  (RAssign StringF tps, PPInfo)
+allocateDebugNames' _ MNil _ ppi = (MNil, ppi)
+allocateDebugNames' base (ds :>: Constant dbg) (CruCtxCons ts tp) ppi =
+  case allocateDebugNames' base ds ts ppi of
+    (outs, ppi1) ->
+      case ppInfoAllocateName str ppi1 of
+        (ppi2, out) -> (outs :>: StringF out, ppi2)
+  where
+    str =
+      case (base,dbg) of
+        (_,Just d) -> "C[" ++ d ++ "]"
+        (Just b,_) -> b ++ "_" ++ typeBaseName tp
+        (Nothing,Nothing) -> typeBaseName tp
 
 -- | FIXME HERE: Make 'ImplM' quantify over any underlying monad, so that we do
 -- not have to use 'traversePermImpl' after we run an 'ImplM'
@@ -2496,9 +2578,8 @@ convertRegType ext loc reg (LLVMPointerRepr w1) (LLVMPointerRepr w2) =
   convertRegType ext loc reg1 (BVRepr w1) (BVRepr w2) >>>= \reg2 ->
   convertRegType ext loc reg2 (BVRepr w2) (LLVMPointerRepr w2)
 convertRegType _ _ x tp1 tp2 =
-  stmtFailM (\i -> pretty "Could not cast" <+> permPretty i x
-                   <+> pretty "from" <+> pretty (show tp1)
-                   <+> pretty "to" <+> pretty (show tp2))
+  permGetPPInfo >>>= \ppinfo ->
+    stmtFailM $ RegisterConversionError (permPretty ppinfo x) tp1 tp2
 
 
 -- | Extract the bitvector of size @sz@ at offset @off@ from a larger bitvector
@@ -2553,10 +2634,11 @@ emitStmt ::
   StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in
     (RAssign Name rets)
 emitStmt tps names loc stmt =
-  gopenBinding
-    ((TypedConsStmt loc stmt (cruCtxProxies tps) <$>) . strongMbM)
-    (mbPure (cruCtxProxies tps) ()) >>>= \(ns, ()) ->
-  setVarTypes Nothing names ns tps >>>
+  let pxys = cruCtxProxies tps in
+  allocateDebugNames Nothing names tps >>>= \debugs ->
+  startBinding' debugs (fmap (TypedConsStmt loc stmt pxys) . strongMbM') >>>= \ns ->
+  modify (\st -> st { stPPInfo = ppInfoApplyAllocation ns debugs (stPPInfo st)}) >>>
+  setVarTypes' ns tps >>>
   gmodify (modifySTCurPerms (applyTypedStmt stmt ns)) >>>
   pure ns
 
@@ -2635,7 +2717,7 @@ ppCruRegAndPerms ctx r =
 -- their permissions, the variables in those permissions etc., as in
 -- 'varPermsTransFreeVars'
 getRelevantPerms :: [SomeName CrucibleType] ->
-                    PermCheckM ext cblocks blocks tops ret r ps r ps 
+                    PermCheckM ext cblocks blocks tops ret r ps r ps
                       (Some DistPerms)
 getRelevantPerms (namesListToNames -> SomeRAssign ns) =
   gets stCurPerms >>>= \perms ->
@@ -2961,7 +3043,7 @@ tcEmitStmt' ctx loc (CallHandle ret freg_untyped _args_ctx args_untyped) =
         _ -> pure Nothing
       _ -> pure []) >>>= \maybe_fun_perms ->
   (stmtEmbedImplM $ foldr1WithDefault implCatchM
-   (implFailMsgM "Could not find function permission")
+   (implFailM FunctionPermissionError)
    (mapMaybe (fmap pure) maybe_fun_perms)) >>>= \some_fun_perm ->
   case some_fun_perm of
     SomeFunPerm fun_perm ->
@@ -2987,7 +3069,7 @@ tcEmitStmt' ctx loc (Assert reg msg) =
   let treg = tcReg ctx reg in
   getRegEqualsExpr treg >>= \case
     PExpr_Bool True -> pure ctx
-    PExpr_Bool False -> stmtFailM (\_ -> pretty "Failed assertion")
+    PExpr_Bool False -> stmtFailM FailedAssertionError
     _ -> ctx <$ emitStmt CruCtxNil MNil loc (TypedAssert (tcReg ctx reg) (tcReg ctx msg))
 
 tcEmitStmt' _ _ _ = error "tcEmitStmt: unsupported statement"
@@ -3013,8 +3095,9 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerExpr w blk_reg off_reg) =
       emitLLVMStmt knownRepr name loc (ConstructLLVMWord toff_reg) >>>= \x ->
       stmtRecombinePerms >>>
       pure (addCtxName ctx x)
-    _ -> stmtFailM (\i -> pretty "LLVM_PointerExpr: Non-zero pointer block: "
-                          <> permPretty i tblk_reg)
+    _ -> 
+      permGetPPInfo >>>= \ppinfo ->
+        stmtFailM $ NonZeroPointerBlockError (permPretty ppinfo tblk_reg)
 
 -- Type-check the LLVM value destructor that gets the block value, by either
 -- proving a permission eq(llvmword e) and returning block 0 or proving
@@ -3119,15 +3202,16 @@ tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions tp conds reg) =
   foldr
   (\(LLVMSideCondition cond_reg ub) rest_m ->
     let tcond_reg = tcReg ctx cond_reg
-        err_str = renderDoc (pretty "Undefined behavior: " <> softline <> UB.explain ub) in
+        err_msg = pretty "Undefined behavior" <> softline <> UB.explain ub in
+        -- err_str = renderDoc (pretty "Undefined behavior: " <> softline <> UB.explain ub) in
     getRegEqualsExpr tcond_reg >>= \case
       PExpr_Bool True ->
         rest_m
-      PExpr_Bool False -> stmtFailM (\_ -> pretty err_str)
+      PExpr_Bool False -> stmtFailM $ UndefinedBehaviorError err_msg
       _ ->
         emitStmt knownRepr noNames loc
           (TypedSetRegPermExpr knownRepr $
-            PExpr_String err_str) >>>= \(MNil :>: str_var) ->
+            PExpr_String (renderDoc err_msg)) >>>= \(_ :>: str_var) ->
         stmtRecombinePerms >>>
         emitStmt CruCtxNil MNil loc
           (TypedAssert tcond_reg $
@@ -3143,7 +3227,7 @@ tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions tp conds reg) =
     pure (addCtxName ctx ret))
   conds
 tcEmitLLVMSetExpr _ctx _loc X86Expr{} =
-  stmtFailM (\_ -> pretty "X86Expr not supported")
+  stmtFailM X86ExprError
 
 
 
@@ -3321,14 +3405,15 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_Alloca w _ sz_reg _ _) =
       stmtRecombinePerms >>>
       pure (addCtxName ctx y)
     (_, _, Nothing) ->
-      stmtFailM (\i -> pretty "LLVM_Alloca: non-constant size for"
-                       <+> permPretty i sz_treg)
+      permGetPPInfo >>>= \ppinfo ->
+        stmtFailM $ AllocaError (AllocaNonConstantError $ permPretty ppinfo sz_treg)
     (Just fp, p, _) ->
-      stmtFailM (\i -> pretty "LLVM_Alloca: expected LLVM frame perm for "
-                       <+> permPretty i fp <> pretty ", found perm"
-                       <+> permPretty i p)
+      permGetPPInfo >>>= \ppinfo ->
+        stmtFailM $ AllocaError $ AllocaFramePermError 
+                                    (permPretty ppinfo fp) 
+                                    (permPretty ppinfo p)
     (Nothing, _, _) ->
-      stmtFailM (const $ pretty "LLVM_Alloca: no frame pointer set")
+      stmtFailM $ AllocaError AllocaFramePtrError
 
 -- Type-check a push frame instruction
 tcEmitLLVMStmt _arch ctx loc (LLVM_PushFrame _ _) =
@@ -3359,7 +3444,7 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PopFrame _) =
           (TypedLLVMDeleteFrame fp fperms del_perms) >>>= \y ->
         modify (\st -> st { stExtState = PermCheckExtState_LLVM Nothing }) >>>
         pure (addCtxName ctx y)
-    _ -> stmtFailM (const $ pretty "LLVM_PopFrame: no frame perms")
+    _ -> stmtFailM $ PopFrameError
 
 -- Type-check a pointer offset instruction by emitting OffsetLLVMValue
 tcEmitLLVMStmt _arch ctx loc (LLVM_PtrAddOffset _w _ ptr off) =
@@ -3391,7 +3476,7 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_LoadHandle _ _ ptr args ret) =
         (TypedLLVMLoadHandle tptr tp p) >>>= \ret' ->
         stmtRecombinePerms >>>
         pure (addCtxName ctx ret')
-    _ -> stmtFailM (const $ pretty "LLVM_PopFrame: no function pointer perms")
+    _ -> stmtFailM LoadHandleError
 
 -- Type-check a ResolveGlobal instruction by looking up the global symbol
 tcEmitLLVMStmt _arch ctx loc (LLVM_ResolveGlobal w _ gsym) =
@@ -3404,8 +3489,7 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_ResolveGlobal w _ gsym) =
       stmtRecombinePerms >>>
       pure (addCtxName ctx ret)
     Nothing ->
-      stmtFailM (const $ pretty ("LLVM_ResolveGlobal: no perms for global "
-                                 ++ globalSymbolName gsym))
+      stmtFailM $ ResolveGlobalError gsym
 
 {-
 tcEmitLLVMStmt _arch ctx loc (LLVM_PtrLe _ r1 r2) =
@@ -3566,9 +3650,10 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr)
     -- If we don't know any relationship between the two registers, then we
     -- fail, because there is no way to compare pointers in the translation
     _ ->
-      stmtFailM (\i ->
-                  sep [pretty "Could not compare LLVM pointer values",
-                       permPretty i x1, pretty "and", permPretty i x2])
+      permGetPPInfo >>>= \ppinfo ->
+        stmtFailM $ PointerComparisonError 
+                      (permPretty ppinfo x1)
+                      (permPretty ppinfo x2)
 
 tcEmitLLVMStmt _arch ctx loc LLVM_Debug{} =
 --  let tptr = tcReg ctx ptr in
@@ -3937,27 +4022,30 @@ tcBlockEntryBody ::
   Block ext cblocks ret args ->
   TypedEntry TCPhase ext blocks tops ret (CtxToRList args) ghosts ->
   TopPermCheckM ext cblocks blocks tops ret
-    (Mb ((tops :++: CtxToRList args) :++: ghosts)
+     (Mb' ((tops :++: CtxToRList args) :++: ghosts)
       (TypedStmtSeq ext blocks tops ret ((tops :++: CtxToRList args) :++: ghosts)))
 tcBlockEntryBody names blk entry@(TypedEntry {..}) =
-  runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $
-  \tops_ns args_ns ghosts_ns perms ->
-  let ctx = mkCtxTrans (blockInputs blk) args_ns
-      ns = RL.append (RL.append tops_ns args_ns) ghosts_ns in
-  stmtTraceM (\i ->
-               pretty "Type-checking block" <+> pretty (blockID blk) <>
-               comma <+> pretty "entrypoint" <+> pretty (entryIndex typedEntryID)
-               <> line <>
-               pretty "Input types:"
-               <> align (permPretty i $
-                         RL.map2 VarAndType ns $ cruCtxToTypes $
-                         typedEntryAllArgs entry)
-               <> line <>
-               pretty "Input perms:"
-               <> align (permPretty i perms)) >>>
-  stmtRecombinePerms >>>
-  tcEmitStmtSeq names ctx (blk ^. blockStmts)
+        runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $
+      \tops_ns args_ns ghosts_ns perms ->
+      let ctx = mkCtxTrans (blockInputs blk) args_ns
+          ns = RL.append (RL.append tops_ns args_ns) ghosts_ns in
+      stmtTraceM (\i ->
+                  pretty "Type-checking block" <+> pretty (blockID blk) <>
+                  comma <+> pretty "entrypoint" <+> pretty (entryIndex typedEntryID)
+                  <> line <>
+                  pretty "Input types:"
+                  <> align (permPretty i $
+                            RL.map2 VarAndType ns $ cruCtxToTypes $
+                            typedEntryAllArgs entry)
+                  <> line <>
+                  pretty "Input perms:"
+                  <> align (permPretty i perms)) >>>
+      stmtRecombinePerms >>>
+      tcEmitStmtSeq names ctx (blk ^. blockStmts)
 
+rappend :: RAssign f x -> RAssign f y -> RAssign f (x :++: y)
+rappend xs (ys :>: y) = rappend xs ys :>: y
+rappend xs MNil = xs
 
 -- | Prove that the permissions held at a call site from the given source
 -- entrypoint imply the supplied input permissions of the current entrypoint
@@ -3971,7 +4059,7 @@ proveCallSiteImpl ::
                                              ((tops :++: args) :++: vars)
                                              tops args ghosts)
 proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out =
-  fmap CallSiteImpl $ runPermCheckM [] srcID args vars mb_perms_in $
+  fmap (CallSiteImpl . _mbBinding) $ runPermCheckM [] srcID args vars mb_perms_in $
   \tops_ns args_ns _ perms_in ->
   let perms_out =
         give (cruCtxProxies ghosts) $
@@ -4019,19 +4107,23 @@ visitCallSite (TypedEntry {..}) site@(TypedCallSite {..})
 
 -- | Widen the permissions held by all callers of an entrypoint to compute new,
 -- weaker input permissions that can hopefully be satisfied by them
-widenEntry :: PermCheckExtC ext =>
-              TypedEntry TCPhase ext blocks tops ret args ghosts ->
-              Some (TypedEntry TCPhase ext blocks tops ret args)
+widenEntry ::
+  forall ext blocks tops ret args ghosts.
+  PermCheckExtC ext =>
+  TypedEntry TCPhase ext blocks tops ret args ghosts ->
+  Some (TypedEntry TCPhase ext blocks tops ret args)
 widenEntry (TypedEntry {..}) =
   trace ("Widening entrypoint: " ++ show typedEntryID) $
   case foldl1' (widen typedEntryTops typedEntryArgs) $
        map (fmapF typedCallSiteArgVarPerms) typedEntryCallers of
-    Some (ArgVarPerms ghosts perms_in) ->
+    Some (ArgVarPerms (ghosts :: CruCtx x) perms_in) ->
       let callers =
-            map (fmapF (callSiteSetGhosts ghosts)) typedEntryCallers in
+            map (fmapF (callSiteSetGhosts ghosts)) typedEntryCallers
+      in
       Some $
       TypedEntry { typedEntryCallers = callers, typedEntryGhosts = ghosts,
-                   typedEntryPermsIn = perms_in, typedEntryBody = Nothing, .. }
+                   typedEntryPermsIn = perms_in, typedEntryBody = Nothing,
+                   .. }
 
 -- | Visit an entrypoint, by first proving the required implications at each
 -- call site, meaning that the permissions held at the call site imply the input
@@ -4076,7 +4168,8 @@ visitEntry names can_widen blk entry =
     else
       do body <- maybe (tcBlockEntryBody names blk entry) return (typedEntryBody entry)
          return $ Some $ entry { typedEntryCallers = callers,
-                                 typedEntryBody = Just body }
+                                 typedEntryBody = Just body
+                                }
 
 
 -- | Visit a block by visiting all its entrypoints
@@ -4164,3 +4257,90 @@ tcCFG w env endianness fun_perm cfg =
                         (visitBlock (rem_iters > 0) >=>
                          assign (stBlockMap . member memb))) >>
           main_loop (rem_iters - 1) nodes
+
+--------------------------------------------------------------------------------
+-- Error handling and logging
+
+data StmtError where
+  AtomicPermError :: Doc ann -> Doc ann -> StmtError
+  RegisterConversionError
+    :: (Show tp1, Show tp2)
+    => Doc ann -> tp1 -> tp2 -> StmtError
+  FailedAssertionError :: StmtError
+  NonZeroPointerBlockError :: Doc ann -> StmtError
+  UndefinedBehaviorError :: Doc () -> StmtError
+  X86ExprError :: StmtError
+  AllocaError :: AllocaErrorType -> StmtError
+  PopFrameError :: StmtError
+  LoadHandleError :: StmtError
+  ResolveGlobalError :: GlobalSymbol -> StmtError
+  PointerComparisonError :: Doc ann -> Doc ann -> StmtError
+
+data AllocaErrorType where
+  AllocaNonConstantError :: Doc ann -> AllocaErrorType
+  AllocaFramePermError :: Doc ann -> Doc ann -> AllocaErrorType
+  AllocaFramePtrError :: AllocaErrorType
+
+instance ErrorPretty StmtError where
+  ppError (AtomicPermError r p) = renderDoc $
+    sep [pretty "getAtomicOrWordLLVMPerms:",
+         pretty "Needed atomic permissions for" <+> r,
+         pretty "but found" <+> p]
+  ppError (RegisterConversionError docx tp1 tp2) = renderDoc $
+    pretty "Could not cast" <+> docx <+>
+    pretty "from" <+> pretty (show tp1) <+>
+    pretty "to" <+> pretty (show tp2)
+  ppError FailedAssertionError = 
+    "Failed assertion"
+  ppError (NonZeroPointerBlockError tblk_reg) = renderDoc $
+    pretty "LLVM_PointerExpr: Non-zero pointer block: " <> tblk_reg
+  ppError (UndefinedBehaviorError doc) = 
+    renderDoc doc
+  ppError X86ExprError = 
+    "X86Expr not supported"
+  ppError (AllocaError (AllocaNonConstantError sz_treg)) = renderDoc $
+    pretty "LLVM_Alloca: non-constant size for" <+>
+    sz_treg
+  ppError (AllocaError (AllocaFramePermError fp p)) = renderDoc $
+    pretty "LLVM_Alloca: expected LLVM frame perm for " <+>
+    fp <> pretty ", found perm" <+> p
+  ppError (AllocaError AllocaFramePtrError) =
+    "LLVM_Alloca: no frame pointer set"
+  ppError PopFrameError =
+    "LLVM_PopFrame: no frame perms"
+  ppError LoadHandleError =
+    "LLVM_LoadHandle: no function pointer perms"
+  ppError (ResolveGlobalError gsym) =
+    "LLVM_ResolveGlobal: no perms for global " ++
+    globalSymbolName gsym
+  ppError (PointerComparisonError x1 x2) = renderDoc $
+    sep [ pretty "Could not compare LLVM pointer values"
+        , x1, pretty "and", x2 ]
+
+
+-- | Get the current 'PPInfo'
+permGetPPInfo :: PermCheckM ext cblocks blocks tops ret r ps r ps PPInfo
+permGetPPInfo = gets stPPInfo
+
+-- | Get the current prefix string to give context to error messages
+getErrorPrefix :: PermCheckM ext cblocks blocks tops ret r ps r ps (Doc ())
+getErrorPrefix = gets (fromMaybe emptyDoc . stErrPrefix)
+
+-- | Emit debugging output using the current 'PPInfo'
+stmtTraceM :: (PPInfo -> Doc ()) ->
+              PermCheckM ext cblocks blocks tops ret r ps r ps String
+stmtTraceM f =
+  do doc <- f <$> permGetPPInfo
+     let str = renderDoc doc
+     trace str (pure str)
+
+-- | Failure in the statement permission-checking monad
+stmtFailM :: StmtError -> PermCheckM ext cblocks blocks tops ret r1 ps1
+             (TypedStmtSeq ext blocks tops ret ps2) ps2 a
+stmtFailM err =
+  getErrorPrefix >>>= \err_prefix ->
+  stmtTraceM (const $ err_prefix <> line <>
+                pretty "Type-checking failure:" <> softline <>
+                pretty (ppError err)) >>>= \str ->
+  gabortM (return $ TypedImplStmt $ AnnotPermImpl str $
+           PermImpl_Step (Impl1_Fail $ GeneralError (pretty "")) MbPermImpls_Nil)
diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs
index 1900049dd8..81ab26f06a 100644
--- a/src/SAWScript/HeapsterBuiltins.hs
+++ b/src/SAWScript/HeapsterBuiltins.hs
@@ -45,6 +45,7 @@ module SAWScript.HeapsterBuiltins
        , heapster_print_fun_trans
        , heapster_export_coq
        , heapster_parse_test
+       , heapster_dump_ide_info
        ) where
 
 import Data.Maybe
@@ -108,6 +109,7 @@ import Verifier.SAW.Heapster.SAWTranslation
 import Verifier.SAW.Heapster.IRTTranslation
 import Verifier.SAW.Heapster.PermParser
 import Verifier.SAW.Heapster.ParsedCtx
+import qualified Verifier.SAW.Heapster.IDESupport as HIDE
 
 import SAWScript.Prover.Exporter
 import Verifier.SAW.Translation.Coq
@@ -270,10 +272,12 @@ heapster_init_env _bic _opts mod_str llvm_filename =
      liftIO $ scLoadModule sc (insImport (const True) preludeMod $
                                  emptyModule saw_mod_name)
      perm_env_ref <- liftIO $ newIORef heapster_default_env
+     tcfg_ref <- liftIO $ newIORef []
      return $ HeapsterEnv {
        heapsterEnvSAWModule = saw_mod_name,
        heapsterEnvPermEnvRef = perm_env_ref,
-       heapsterEnvLLVMModules = [llvm_mod]
+       heapsterEnvLLVMModules = [llvm_mod],
+       heapsterEnvTCFGs = tcfg_ref
        }
 
 load_sawcore_from_file :: BuiltinContext -> Options -> String -> TopLevel ()
@@ -290,10 +294,12 @@ heapster_init_env_from_file _bic _opts mod_filename llvm_filename =
      (saw_mod, saw_mod_name) <- readModuleFromFile mod_filename
      liftIO $ tcInsertModule sc saw_mod
      perm_env_ref <- liftIO $ newIORef heapster_default_env
+     tcfg_ref <- liftIO $ newIORef []
      return $ HeapsterEnv {
        heapsterEnvSAWModule = saw_mod_name,
        heapsterEnvPermEnvRef = perm_env_ref,
-       heapsterEnvLLVMModules = [llvm_mod]
+       heapsterEnvLLVMModules = [llvm_mod],
+       heapsterEnvTCFGs = tcfg_ref
        }
 
 heapster_init_env_for_files :: BuiltinContext -> Options -> String -> [String] ->
@@ -304,10 +310,12 @@ heapster_init_env_for_files _bic _opts mod_filename llvm_filenames =
      (saw_mod, saw_mod_name) <- readModuleFromFile mod_filename
      liftIO $ tcInsertModule sc saw_mod
      perm_env_ref <- liftIO $ newIORef heapster_default_env
+     tcfg_ref <- liftIO $ newIORef []
      return $ HeapsterEnv {
        heapsterEnvSAWModule = saw_mod_name,
        heapsterEnvPermEnvRef = perm_env_ref,
-       heapsterEnvLLVMModules = llvm_mods
+       heapsterEnvLLVMModules = llvm_mods,
+       heapsterEnvTCFGs = tcfg_ref
        }
 
 -- | Look up the CFG associated with a symbol name in a Heapster environment
@@ -350,7 +358,7 @@ heapster_define_recursive_perm _bic _opts henv
        Some args_ctx <- parseParsedCtxString "argument types" env args_str
        let args = parsedCtxCtx args_ctx
        Some tp <- parseTypeString "permission type" env tp_str
-       trans_tp <- liftIO $ 
+       trans_tp <- liftIO $
          translateCompleteTypeInCtx sc env args (nus (cruCtxProxies args) $
                                                  const $ ValuePermRepr tp)
        trans_ident <- parseAndInsDef henv nm trans_tp trans_str
@@ -559,7 +567,7 @@ heapster_define_reachability_perm _bic _opts henv
               _ -> Fail.fail "Incorrect type for last argument of reachability perm"
        let args_ctx = appendParsedCtx pre_args_ctx last_args_ctx
        let args = parsedCtxCtx args_ctx
-       trans_tp <- liftIO $ 
+       trans_tp <- liftIO $
          translateCompleteTypeInCtx sc env args (nus (cruCtxProxies args) $
                                                  const $ ValuePermRepr tp)
        trans_tp_ident <- parseAndInsDef henv nm trans_tp trans_tp_str
@@ -964,7 +972,7 @@ heapster_typecheck_mut_funs :: BuiltinContext -> Options -> HeapsterEnv ->
                                [(String, String)] -> TopLevel ()
 heapster_typecheck_mut_funs bic opts henv =
   heapster_typecheck_mut_funs_rename bic opts henv .
-  map (\(nm, perms_string) -> (nm, nm, perms_string)) 
+  map (\(nm, perms_string) -> (nm, nm, perms_string))
 
 heapster_typecheck_mut_funs_rename ::
   BuiltinContext -> Options -> HeapsterEnv ->
@@ -999,10 +1007,11 @@ heapster_typecheck_mut_funs_rename _bic _opts henv fn_names_and_perms =
                                   fromString nm) nm_to cfg fun_perm)
      sc <- getSharedContext
      let saw_modname = heapsterEnvSAWModule henv
-     env' <- liftIO $
+     (env', tcfgs) <- liftIO $
        let ?ptrWidth = w in
        tcTranslateAddCFGs sc saw_modname env endianness some_cfgs_and_perms
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
+     liftIO $ modifyIORef (heapsterEnvTCFGs henv) (\old -> map Some tcfgs ++ old)
 
 
 heapster_typecheck_fun :: BuiltinContext -> Options -> HeapsterEnv ->
@@ -1020,7 +1029,7 @@ heapster_typecheck_fun_rename bic opts henv fn_name fn_name_to perms_string =
 heapster_typecheck_fun_rs :: BuiltinContext -> Options -> HeapsterEnv ->
                              String -> String -> TopLevel ()
 heapster_typecheck_fun_rs bic opts henv fn_name perms_string =
-  heapster_typecheck_fun bic opts henv 
+  heapster_typecheck_fun bic opts henv
 
 heapster_typecheck_fun_rename_rs :: BuiltinContext -> Options -> HeapsterEnv ->
                                     String -> String -> String -> TopLevel ()
@@ -1065,3 +1074,10 @@ heapster_parse_test _bic _opts _some_lm@(Some lm) fn_name perms_string =
      SomeFunPerm fun_perm <- parseFunPermString "permissions" env args
                                                 ret perms_string
      liftIO $ putStrLn $ permPrettyString emptyPPInfo fun_perm
+
+heapster_dump_ide_info :: BuiltinContext -> Options -> HeapsterEnv -> String -> TopLevel ()
+heapster_dump_ide_info _bic _opts henv filename = do
+  -- heapster_typecheck_mut_funs bic opts henv [(fnName, perms)]
+  penv <- io $ readIORef (heapsterEnvPermEnvRef henv)
+  tcfgs <- io $ readIORef (heapsterEnvTCFGs henv)
+  io $ HIDE.printIDEInfo penv tcfgs filename emptyPPInfo
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index fcfc5630b8..82df0e0c18 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -3271,6 +3271,13 @@ primitives = Map.fromList
     [ "Parse and print back a set of Heapster permissions for a function"
     ]
 
+  , prim "heapster_dump_ide_info"
+    "HeapsterEnv -> String -> TopLevel ()"
+    (bicVal heapster_dump_ide_info)
+    Experimental
+    [ "Dump environment info to a JSON file for IDE integration."
+    ]
+
     ---------------------------------------------------------------------
 
   , prim "sharpSAT"  "Term -> TopLevel Integer"
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 7748fc78a5..cef70c21c6 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -110,6 +110,7 @@ import Lang.Crucible.LLVM.ArraySizeProfile
 import           What4.ProgramLoc (ProgramLoc(..))
 
 import Verifier.SAW.Heapster.Permissions
+import Verifier.SAW.Heapster.TypedCrucible (SomeTypedCFG(..))
 
 -- Values ----------------------------------------------------------------------
 
@@ -182,8 +183,10 @@ data HeapsterEnv = HeapsterEnv {
   -- ^ The SAW module containing all our Heapster definitions
   heapsterEnvPermEnvRef :: IORef PermEnv,
   -- ^ The current permissions environment
-  heapsterEnvLLVMModules :: [Some CMSLLVM.LLVMModule]
+  heapsterEnvLLVMModules :: [Some CMSLLVM.LLVMModule],
   -- ^ The list of underlying 'LLVMModule's that we are translating
+  heapsterEnvTCFGs :: IORef [Some SomeTypedCFG]
+  -- ^ The typed CFGs for output debugging/IDE info
   }
 
 showHeapsterEnv :: HeapsterEnv -> String