diff --git a/heapster-saw/heapster-saw.cabal b/heapster-saw/heapster-saw.cabal
index 02a65a041c..de796b54d1 100644
--- a/heapster-saw/heapster-saw.cabal
+++ b/heapster-saw/heapster-saw.cabal
@@ -38,7 +38,10 @@ library
     filepath,
     language-rust,
     hobbits ^>= 1.4,
-    extra,
+    aeson ^>= 1.5,
+    th-abstraction,
+    template-haskell,
+    extra
   hs-source-dirs: src
   build-tool-depends:
     alex:alex,
@@ -46,12 +49,15 @@ library
   exposed-modules:
     Verifier.SAW.Heapster.CruUtil
     Verifier.SAW.Heapster.GenMonad
+    Verifier.SAW.Heapster.IDESupport
     Verifier.SAW.Heapster.HintExtract
     Verifier.SAW.Heapster.Implication
     Verifier.SAW.Heapster.IRTTranslation
     Verifier.SAW.Heapster.Lexer
     Verifier.SAW.Heapster.LLVMGlobalConst
     Verifier.SAW.Heapster.Located
+    Verifier.SAW.Heapster.NamedMb
+    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 e4c09c3703..a864a538d7 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs
@@ -25,6 +25,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
@@ -570,6 +571,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..f70a89cbae 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs
@@ -8,17 +8,20 @@ module Verifier.SAW.Heapster.GenMonad (
   -- * Core definitions
   GenStateContT(..), (>>>=), (>>>),
   -- * Continuation operations
-  gcaptureCC, gmapRet, gabortM, gparallel, gopenBinding,
+  gcaptureCC, gmapRet, gabortM, gparallel, startBinding,
+  startNamedBinding, gopenBinding, gopenNamedBinding,
   -- * 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 +110,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)
+gopenNamedBinding ::
+  (NamedMb ctx (m b1) -> m r2) ->
+  NamedMb ctx b2 ->
+  GenStateContT s b1 s r2 m (RAssign Name ctx, b2)
+gopenNamedBinding f_ret mb_a =
+  gcaptureCC \k ->
+  f_ret $ flip nuMultiWithElim1Named 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)
+startNamedBinding ::
+  RAssign StringF ctx ->
+  (NamedMb ctx (m r1) -> m r2) ->
+  GenStateContT s r1 s r2 m (RAssign Name ctx)
+startNamedBinding tps f_ret = gcaptureCC (f_ret . nuMultiNamed 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..b86c58b836
--- /dev/null
+++ b/heapster-saw/src/Verifier/SAW/Heapster/IDESupport.hs
@@ -0,0 +1,331 @@
+{-# 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.Permissions
+import Verifier.SAW.Heapster.Implication
+import Verifier.SAW.Heapster.TypedCrucible
+import Verifier.SAW.Heapster.SAWTranslation (SomeTypedCFG (..))
+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 extExpr)
+    => ExtractLogEntries
+         (TypedEntry TransPhase ext blocks tops ret args ghosts) where
+  extractLogEntries te = do
+    let loc = mbLiftNamed $ 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 extExpr)
+  => ExtractLogEntries (TypedCFG ext blocks ghosts inits gouts ret) where
+    extractLogEntries tcfg = extractLogEntries $ tpcfgBlockMap tcfg
+
+instance (PermCheckExtC ext extExpr)
+  => ExtractLogEntries (TypedBlockMap TransPhase ext blocks tops ret) where
+  extractLogEntries tbm =
+    sequence_ $ RL.mapToList extractLogEntries tbm
+
+instance (PermCheckExtC ext extExpr)
+  => 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 => NamedMb (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 gouts ret -> String
+getFunctionName tcfg = case tpcfgHandle tcfg of
+  TypedFnHandle _ _ handle -> show $ handleName handle
+
+getFirstProgramLoc
+  :: PermCheckExtC ext extExpr
+  => TypedCFG ext blocks ghosts inits gouts 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 extExpr
+  => TypedBlock TransPhase ext blocks tops ret ctx
+  -> Maybe ProgramLoc
+getFirstProgramLocBM block =
+  listToMaybe $ mapMaybe helper (_typedBlockEntries block)
+  where
+    helper
+      :: PermCheckExtC ext extExpr
+      => Some (TypedEntry TransPhase ext blocks tops ret ctx)
+      -> Maybe ProgramLoc
+    helper ste = case ste of
+      Some TypedEntry { typedEntryBody = stmts } ->
+        Just $ mbLiftNamed $ 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 extExpr
+  => TypedStmtSeq ext blocks tops ret ctx
+  -> ProgramLoc
+getFirstProgramLocTS (TypedImplStmt (AnnotPermImpl _ pis)) =
+  getFirstProgramLocPI pis
+getFirstProgramLocTS (TypedConsStmt loc _ _ _) = loc
+getFirstProgramLocTS (TypedTermStmt loc _) = loc
+
+getFirstProgramLocPI
+  :: PermCheckExtC ext extExpr
+  => PermImpl (TypedStmtSeq ext blocks tops ret) ctx
+  -> ProgramLoc
+getFirstProgramLocPI (PermImpl_Done stmts) = getFirstProgramLocTS stmts
+getFirstProgramLocPI (PermImpl_Step _ mbps) = getFirstProgramLocMBPI mbps
+
+getFirstProgramLocMBPI
+  :: PermCheckExtC ext extExpr
+  => 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 889a234fc0..392120d423 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -68,6 +68,8 @@ import Verifier.SAW.Heapster.GenMonad
 import GHC.Stack
 import Unsafe.Coerce
 import Data.Functor.Constant (Constant(..))
+import Data.Functor.Product (Product(..))
+
 
 
 ----------------------------------------------------------------------
@@ -353,6 +355,81 @@ 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
+
+$(concatMapM mkNuMatching
+  [ [t| ImplError |]
+  , [t| LifetimeErrorType |]
+  ])
+
+instance Liftable LifetimeErrorType where
+  mbLift e = case mbMatch e of
+    [nuMP| EndLifetimeError |] -> EndLifetimeError
+    [nuMP| ImplicationLifetimeError |] -> ImplicationLifetimeError
+    [nuMP| LifetimeCurrentError doc |] -> LifetimeCurrentError $ mbLift doc
+
+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
+   
+-- 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
 ----------------------------------------------------------------------
@@ -1380,7 +1457,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:
@@ -1677,12 +1754,12 @@ permImplStep impl1@(Impl1_TryProveBVProp _ _ _) mb_impls =
   permImplStepUnary impl1 mb_impls
 
 -- An or elimination fails if both branches fail
-permImplStep (Impl1_ElimOrs _ _ _) (MbPermImpls_Cons _
-                                    (MbPermImpls_Cons _ MbPermImpls_Nil
-                                     (matchMbImplFail -> Just msg1))
-                                    (matchMbImplFail -> Just msg2)) =
-  PermImpl_Step (Impl1_Fail
-                 (msg1 ++ "\n\n--------------------\n\n" ++ msg2))
+permImplStep (Impl1_ElimOr _ _ _) (MbPermImpls_Cons _
+                                   (MbPermImpls_Cons _ MbPermImpls_Nil
+                                    (matchMbImplFail -> Just msg1))
+                                   (matchMbImplFail -> Just msg2)) =
+  PermImpl_Step (Impl1_Fail $ GeneralError $ pretty
+                  (msg1 ++ "\n\n--------------------\n\n" ++ msg2))
   MbPermImpls_Nil
 
 -- Default case: just apply PermImpl_Step
@@ -1698,7 +1775,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
@@ -1721,7 +1798,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
@@ -1749,7 +1826,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
@@ -3174,7 +3253,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
@@ -3465,12 +3544,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 substitution 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) ->
@@ -3573,7 +3651,7 @@ implRecFlagCaseM f p 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
@@ -3582,7 +3660,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
@@ -3715,6 +3793,34 @@ implSetNameTypes (ns :>: n) (CruCtxCons tps tp) =
      handleUnitVar tp 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 x p = NameSet.member x (freeVars p)
+
+-- | Build a 'DistPerms' sequence of a permission @y1:p1@ we currently hold such
+-- that @p1@ contains @x@, a permission @y2:p2@ we currently hold such that @p2@
+-- contains @p1@, etc.
+--
+-- FIXME: what is the purpose of this? Don't we want all permissions recursively
+-- containing @x@?
+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
+      
 -- | When adding a new existential unit-typed variable, instantiate it with the
 -- underlying global unit if available; if not, update the global unit variable
 -- with a fresh variable
@@ -3754,7 +3860,6 @@ handleUnitEVars =
                        ImplM vars s r ps ps ()
     handleUnitEVarM mem m = handleUnitEVar mem >>> m
 
-
 -- | When adding a new universal unit-typed variable, unify with the underlying
 -- global unit if available, and if not, update the global unit variable with
 -- the variable provided
@@ -3869,18 +3974,6 @@ implWithoutTracingM m =
   (implStateDebugLevel .= 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
@@ -3889,15 +3982,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. The supplied 'String' says what
 -- proof-search function is performing the catch, while the @p@ argument says
@@ -4197,7 +4281,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 ()
@@ -4760,8 +4844,7 @@ implEndLifetimeM ps l tps_in tps_out ps_in ps_out
     implTraceM (\i -> pretty "Ending lifetime:" <+> permPretty i l) >>>
     implDropLifetimePermsM l >>>
     recombinePermsPartial ps (DistPermsCons dps_out l ValPerm_LFinished)
-implEndLifetimeM _ _ _ _ _ _ =
-  implFailM "implEndLifetimeM: exprPermsToDistPerms"
+implEndLifetimeM _ _ _ _ _ _ = implFailM (LifetimeError EndLifetimeError)
 
 -- | Drop any permissions of the form @x:[l]p@ in the primary permissions for
 -- @x@, which are supplied as an argument
@@ -5448,9 +5531,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)
 
 -- | Destruct a shape @sh1 orsh (sh2 orsh (... orsh shn))@ that is a
 -- right-nested disjunctive shape into the list @[sh1,...,shn]@ of disjuncts
@@ -5658,9 +5740,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 ->
@@ -5951,16 +6032,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
@@ -5999,7 +6070,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 =
@@ -6086,7 +6161,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 &+ o = e@, we subtract @o@ from the RHS and recurse
   (PExpr_LLVMOffset x off, _) ->
@@ -6112,7 +6191,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 |])
@@ -6123,7 +6206,11 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
         Just e' ->
           proveEq e (mbConst 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
@@ -6147,7 +6234,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)@
@@ -7158,11 +7248,9 @@ proveVarLLVMArray_FromArrayH x ap_lhs _ bs mb_ap =
      localMbProveVars dps_in dps_out >>>= \mb_impl ->
      implSimplM Proxy (SImpl_LLVMArrayContents x ap_lhs'' sh mb_impl) >>>
      return (ap_lhs'' { llvmArrayCellShape = sh })) >>>= \ap_lhs''' ->
-
   -- Finally, rearrange the borrows of ap_lhs to match bs
   implLLVMArrayRearrange x ap_lhs''' bs
 
-
 ----------------------------------------------------------------------
 -- * Proving Named Permission Arguments
 ----------------------------------------------------------------------
@@ -8444,7 +8532,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
              exprPermsToDistPerms ps_inR, exprPermsToDistPerms 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: exprPermsToDistPerms")
+          _ -> 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 ->
@@ -8635,12 +8723,10 @@ proveVarConjImpl x ps_lhs mb_ps =
       partialSubstForceM mb_p "proveVarConjImpl" >>>= \p ->
       implInsertConjM x p ps' i
     [nuMP| Nothing |] ->
-      implTraceM
-      (\i ->
-        sep [PP.fillSep [PP.pretty
-             "Could not determine enough variables to prove permissions:",
-             permPretty i (mbValPerm_Conj mb_ps)]]) >>>=
-      implFailM
+      use implStatePPInfo >>>= \ppinfo ->
+      implFailM $ InsufficientVariablesError $ 
+      permPretty ppinfo (fmap ValPerm_Conj mb_ps)
+
 
 
 ----------------------------------------------------------------------
@@ -8962,15 +9048,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)
 
 
 ----------------------------------------------------------------------
@@ -9115,14 +9200,10 @@ proveVarsImplAppendInt mb_ps =
         proveVarsImplAppendInt ps12 >>>
         implMoveUpM cur_perms (mbLift prxs1) x (mbLift prxs2)
       else
-        implTraceM
-        (\i ->
-          sep [PP.fillSep
-               [PP.pretty
-                "Could not determine enough variables to prove permissions:",
-                permPretty i mb_ps]]) >>>=
-        implFailM
-
+        use implStatePPInfo >>>= \ppinfo ->
+        implFailM $ InsufficientVariablesError $
+        permPretty ppinfo mb_ps
+        
 -- | Like 'proveVarsImplAppendInt' but re-associate the appends
 proveVarsImplAppendIntAssoc ::
   NuMatchingAny1 r => prx ps_in -> prx1 ps1 -> ExDistPerms vars ps ->
@@ -9224,7 +9305,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
 -- those proofs to the top of the stack. In the case that a the variable itself
@@ -9307,6 +9389,67 @@ 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
+
+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 ]
+
 -- | Try to prove @x:p@, returning whether or not this was successful
 checkVarImpl ::
   PermSet ps_in ->
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..b8a8e05ada
--- /dev/null
+++ b/heapster-saw/src/Verifier/SAW/Heapster/JSONExport.hs
@@ -0,0 +1,211 @@
+{-# 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.LLVM.DataLayout (EndianForm)
+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
+
+
+-- 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,
+        ''LLVMArrayIndex, ''LLVMArrayPerm, ''LLVMBlockPerm, ''LLVMFieldPerm,
+        ''LLVMFieldShape, ''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,
+        ''ExprAndPerm, ''OrListDisj, ''EndianForm
+        ]
+
+ in traverse generateJsonExport typesNeeded
+
+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 PermExpr
+instance JsonExport1 ValuePerm
+instance JsonExport1 VarAndPerm
+instance JsonExport1 Proxy
+instance JsonExport1 ExprAndPerm
+instance JsonExport1 (OrListDisj ps a) 
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..27e1beecc7
--- /dev/null
+++ b/heapster-saw/src/Verifier/SAW/Heapster/NamedMb.hs
@@ -0,0 +1,95 @@
+{-# 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
+
+-- | A constant type functor for 'String's
+newtype StringF a = StringF { unStringF :: String }
+
+mkNuMatching [t| forall a. StringF a |]
+
+-- | An 'Mb' multi-binding where each bound 'Name' has an associated 'String'
+-- for parsing and printing it
+data NamedMb ctx a = NamedMb
+  { _mbNames :: RAssign StringF ctx
+  , _mbBinding :: Mb ctx a
+  }
+  deriving Functor
+
+-- | A 'Binding' of a single 'Name' with a 'String'
+type NamedBinding c = NamedMb (RNil :> c)
+
+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 => NamedMb ctx a |]
+
+-- | Apply a binary function to the body of a 'NamedMb'; similar to 'mbMap2'
+mbMap2Named :: (a -> b -> c) -> NamedMb ctx a -> NamedMb ctx b -> NamedMb ctx c
+mbMap2Named f mb1 mb2 =
+  NamedMb (_mbNames mb1) (mbMap2 f (_mbBinding mb1) (_mbBinding mb2))
+
+-- | A 'Lens' to get the binding ouf of a 'NamedMb'
+mbBinding :: Lens (NamedMb ctx a) (NamedMb ctx b) (Mb ctx a) (Mb ctx b)
+mbBinding f x = NamedMb (_mbNames x) <$> f (_mbBinding x)
+
+-- | Build a 'NamedMb' that binds multiple 'Name's with the given 'String's
+nuMultiNamed :: RAssign StringF ctx -> (RAssign Name ctx -> b) -> NamedMb ctx b
+nuMultiNamed tps f = NamedMb
+  { _mbNames = tps
+  , _mbBinding = nuMulti (mapRAssign (const Proxy) tps) f
+  }
+
+-- | A version of 'nuMultiWithElim1' for 'NamedMb'
+nuMultiWithElim1Named :: (RAssign Name ctx -> arg -> b) ->
+                         NamedMb ctx arg -> NamedMb ctx b
+nuMultiWithElim1Named k = over mbBinding (nuMultiWithElim1 k)
+
+-- | Commute a 'NamedMb' inside a strong binding monad
+strongMbMNamed :: MonadStrongBind m => NamedMb ctx (m a) -> m (NamedMb ctx a)
+strongMbMNamed = traverseOf mbBinding strongMbM
+
+-- | Commute a 'NamedMb' inside a binding monad
+mbMNamed :: (MonadBind m, NuMatching a) => NamedMb ctx (m a) -> m (NamedMb ctx a)
+mbMNamed = traverseOf mbBinding mbM
+
+-- | Swap the order of two nested named bindings
+mbSwapNamed :: RAssign Proxy ctx -> NamedMb ctx' (NamedMb ctx a) ->
+               NamedMb ctx (NamedMb ctx' a)
+mbSwapNamed p (NamedMb names' body') =
+    NamedMb
+    { _mbNames = mbLift (_mbNames <$> body')
+    , _mbBinding = NamedMb names' <$> mbSwap p (_mbBinding <$> body')
+    }
+
+-- | Swap the order of a binding with 'String' names with one without
+mbSink :: RAssign Proxy ctx -> Mb ctx' (NamedMb ctx a) -> NamedMb ctx (Mb ctx' a)
+mbSink p m =
+    NamedMb
+    { _mbNames = mbLift (_mbNames <$> m)
+    , _mbBinding = mbSwap p (_mbBinding <$> m)
+    }
+
+-- | Lift a 'Liftable' value out of a 'NamedMb'
+mbLiftNamed :: Liftable a => NamedMb ctx a -> a
+mbLiftNamed = views mbBinding mbLift
+
+-- | Eliminate a 'NamedMb' that binds zero names
+elimEmptyNamedMb :: NamedMb RNil a -> a
+elimEmptyNamedMb = views mbBinding elimEmptyMb
+
+-- | Create a 'NamedMb' that binds zero names
+emptyNamedMb :: a -> NamedMb RNil a
+emptyNamedMb = NamedMb MNil . emptyMb
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index c34ce7a47b..44926339bc 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -90,6 +90,7 @@ import Verifier.SAW.Term.Functor (ModuleName)
 import Verifier.SAW.Module
 import Verifier.SAW.SharedTerm hiding (Constant)
 import Verifier.SAW.OpenTerm
+import Verifier.SAW.Heapster.NamedMb
 
 import Verifier.SAW.Heapster.CruUtil
 
@@ -1145,9 +1146,6 @@ debugTraceTraceLvl = debugTrace traceDebugLevel
 debugTracePretty :: DebugLevel -> DebugLevel -> Doc ann -> a -> a
 debugTracePretty req dlevel d a = debugTrace req dlevel (renderDoc d) a
 
--- | The constant string functor
-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"
@@ -1184,16 +1182,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) ->
@@ -1202,12 +1208,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
 
@@ -1351,7 +1378,22 @@ permPrettyExprMb :: PermPretty a =>
                     Mb (ctx :: RList CrucibleType) a -> PermPPM (Doc ann)
 permPrettyExprMb f = permPrettyMb (\ns_pp a -> f ns_pp (permPrettyM a))
 
-instance PermPretty a => PermPretty (Mb (ctx :: RList CrucibleType) a) where
+
+-- | Pretty-print an expression-like construct in a name-binding using
+-- a function that combines the pretty-printed names along with the
+-- pretty-printed body of the name-binding, using the types of the
+-- found names to generate their string names
+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
   permPrettyM =
     permPrettyExprMb $ \docs ppm ->
     (\pp -> ppEncList True (RL.toList docs) <> dot <> line <> pp) <$> ppm
@@ -1748,7 +1790,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 $ sep [pretty "exsh" <+> pp_n <> dot, pp]
   permPrettyM PExpr_FalseShape = return $ pretty "falsesh"
@@ -3477,8 +3519,8 @@ 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 ->
-    (\pp -> pretty "exists" <+> pp_n <> dot <+> pp) <$> 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
        args_pp <- permPrettyM args
@@ -3687,7 +3729,6 @@ instance PermPretty (ExprAndPerm a) where
 instance PermPrettyF ExprAndPerm where
   permPrettyMF = permPrettyM
 
-
 -- | Embed a 'ValuePerm' in a 'PermExpr' - like 'PExpr_ValPerm' but maps
 -- 'ValPerm_Var's to 'PExpr_Var's
 permToExpr :: ValuePerm a -> PermExpr (ValuePermType a)
@@ -6722,6 +6763,27 @@ genSubstMb ::
 genSubstMb p s mbmb =
   mbM $ nuMulti p $ \ns -> genSubst (extSubstMulti s ns) (mbCombine p mbmb)
 
+
+instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx),
+                             Substable s a m, NuMatching a) =>
+                            Substable s (NamedMb ctx a) m where
+   genSubst = genSubstNamedMb given
+
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) =>
+                            Substable s (NamedMb RNil a) m where
+   genSubst = genSubstNamedMb RL.typeCtxProxies
+
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) =>
+                            Substable s (NamedBinding c a) m where
+   genSubst = genSubstNamedMb RL.typeCtxProxies
+
+genSubstNamedMb ::
+  Substable s a m =>
+  NuMatching a =>
+  RAssign Proxy ctx ->
+  s ctx' -> Mb ctx' (NamedMb ctx a) -> m (NamedMb ctx a)
+genSubstNamedMb p s mbmb = mbMNamed (fmap (genSubst s) (mbSink p mbmb))
+
 instance SubstVar s m => Substable s (Member ctx a) m where
   genSubst _ mb_memb = return $ mbLift mb_memb
 
@@ -6737,6 +6799,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 =
@@ -8431,7 +8497,7 @@ detVarsClauseAddLHSVar :: ExprVar a -> DetVarsClause -> DetVarsClause
 detVarsClauseAddLHSVar n (DetVarsClause lhs rhs) =
   DetVarsClause (NameSet.insert n lhs) rhs
 
-newtype SeenDetVarsClauses :: CrucibleType -> * where
+newtype SeenDetVarsClauses :: CrucibleType -> Type where
   SeenDetVarsClauses :: [DetVarsClause] -> SeenDetVarsClauses tp
 
 -- | Generic function to compute the 'DetVarsClause's for a permission
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 60e81c39aa..aad0829292 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -76,6 +76,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
 
@@ -3294,7 +3295,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
@@ -3657,7 +3657,8 @@ translatePermImpl1 :: ImplTranslateF r ext blocks tops rets =>
 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) |]) ->
@@ -4497,8 +4498,7 @@ translateCallEntry nm entry_trans mb_tops_args mb_ghosts =
             withPermStackM
               (const $ RL.members ectx)
               (const $ typeTransF perms_trans $ transTerms stack)
-              (translate $ typedEntryBody entry)
-
+              (translate $ _mbBinding $ typedEntryBody entry)
 
 instance PermCheckExtC ext exprExt =>
          Translate (ImpTransInfo ext blocks tops rets ps) ctx
@@ -4812,7 +4812,7 @@ instance PermCheckExtC ext exprExt =>
   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 exprExt =>
@@ -4983,7 +4983,7 @@ translateEntryBody stack mapTrans entry =
   lambdaPermCtx (typedEntryPermsIn entry) $ \pctx ->
   do retType <- translateEntryRetType entry
      impTransM (RL.members pctx) pctx mapTrans stack retType $
-       translate $ typedEntryBody entry
+       translate $ _mbBinding $ typedEntryBody entry
 
 -- | Translate all the entrypoints in a 'TypedBlockMap' that correspond to
 -- letrec-bound functions to SAW core functions as in 'translateEntryBody'
@@ -5087,7 +5087,7 @@ data SomeCFGAndPerm ext where
 -- | An existentially quantified tuple of a 'TypedCFG', its 'GlobalSymbol', and
 -- a 'String' name we want to translate it to
 data SomeTypedCFG ext where
-  SomeTypedCFG :: GlobalSymbol -> String ->
+  SomeTypedCFG :: PermCheckExtC ext exprExt => GlobalSymbol -> String ->
                   TypedCFG ext blocks ghosts inits gouts ret ->
                   SomeTypedCFG ext
 
@@ -5151,7 +5151,7 @@ frameTypeOpenTerm = dataTypeOpenTerm "Prelude.List1" [dataTypeOpenTerm
 tcTranslateAddCFGs ::
   HasPtrWidth w => SharedContext -> ModuleName -> PermEnv -> ChecksFlag ->
   EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] ->
-  IO PermEnv
+  IO (PermEnv, [SomeTypedCFG LLVM])
 tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
   withKnownNat ?ptrWidth $
   do
@@ -5235,7 +5235,7 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
            let perm = mkPtrFunPerm $ tpcfgFunPerm cfg
            return $ PermEnvGlobalEntry sym perm (Right [globalOpenTerm ident]))
       tcfgs fun_ixs
-    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 4a5cb4ee26..d91c3d3e8d 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -52,7 +52,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)
@@ -82,6 +81,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 GHC.Stack (HasCallStack)
 
@@ -376,7 +376,6 @@ instance Closable (TypedCallSiteID blocks args vars) where
 instance Liftable (TypedCallSiteID blocks args vars) where
   mbLift = unClosed . mbLift . fmap toClosed
 
-
 ----------------------------------------------------------------------
 -- * Typed Crucible Statements
 ----------------------------------------------------------------------
@@ -767,7 +766,7 @@ data TypedStmtSeq ext blocks tops rets ps_in where
   TypedConsStmt :: !ProgramLoc ->
                    !(TypedStmt ext stmt_rets ps_in ps_next) ->
                    !(RAssign Proxy stmt_rets) ->
-                   !(Mb stmt_rets (TypedStmtSeq ext blocks tops rets ps_next)) ->
+                   !(NamedMb stmt_rets (TypedStmtSeq ext blocks tops rets ps_next)) ->
                    TypedStmtSeq ext blocks tops rets ps_in
 
   -- | Typed version of 'TermStmt', which terminates the current block
@@ -1208,11 +1207,12 @@ data TypedEntry phase ext blocks tops rets args ghosts =
     typedEntryPermsOut :: !(MbValuePerms (tops :++: rets)),
     -- | The type-checked body of the entrypoint
     typedEntryBody :: !(TransData phase
-                        (Mb ((tops :++: args) :++: ghosts)
+                        (NamedMb ((tops :++: args) :++: ghosts)
                          (TypedStmtSeq ext blocks tops rets
                           ((tops :++: args) :++: ghosts))))
   }
 
+
 -- | Test if an entrypoint has in-degree greater than 1
 typedEntryHasMultiInDegree :: TypedEntry phase ext blocks tops rets args ghosts ->
                               Bool
@@ -1971,26 +1971,74 @@ runPermCheckM ::
               () ps_out
               r ((tops :++: args) :++: ghosts)
               ()) ->
-  TopPermCheckM ext cblocks blocks tops rets (Mb ((tops :++: args) :++: ghosts) r)
+  TopPermCheckM ext cblocks blocks tops rets (NamedMb ((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 $ strongMbMNamed $
+  flip nuMultiWithElim1Named (NamedMb 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
+
+  allocateDebugNamesM (Just "top") (noNames' topCtx) topCtx >>>= \topDbgs ->
+  allocateDebugNamesM (Just "local") arg_names argCtx >>>= \argDbgs ->
+  allocateDebugNamesM (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
@@ -2159,11 +2207,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
@@ -2179,11 +2224,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 ::
@@ -2262,39 +2307,55 @@ stmtHandleUnitVars ns =
 
 -- | Remember the type of a free variable, and ensure that it has a permission
 setVarType ::
-  Maybe String {- ^ The base name of the variable (e.g., "top", "arg", etc.) -} ->
-  Maybe String {- ^ The C name of the variable, if applicable -} ->
-  ExprVar a    {- ^ The Hobbits variable itself -} ->
-  TypeRepr a   {- ^ The type of the variable -} ->
-  PermCheckM ext cblocks blocks tops rets r ps r ps ()
-setVarType maybe_str dbg x tp =
-    (modify $ \st ->
-         st { stCurPerms = initVarPerm x (stCurPerms st),
-              stVarTypes = NameMap.insert x tp (stVarTypes st),
-              stPPInfo   = ppInfoAddExprName (dbgStringPP maybe_str dbg tp)
-                                             x
-                                            (stPPInfo st)
-         })
+  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) }
 
 -- | Remember the types of a sequence of free variables
 setVarTypes ::
-  Maybe String {- ^ The bsae name of the variable (e.g., "top", "arg", etc.) -} ->
-  RAssign (Constant (Maybe String)) tps ->
   RAssign Name tps ->
   CruCtx tps ->
-  PermCheckM ext cblocks blocks tops rets r ps r ps ()
-setVarTypes _ MNil MNil CruCtxNil = pure ()
-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 rets 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 rets r ps r ps (Doc ())
-getErrorPrefix = gets (fromMaybe emptyDoc . stErrPrefix)
+  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
+
+allocateDebugNames ::
+  Maybe String -> -- ^ The base 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
+
+        
+allocateDebugNamesM ::
+  Maybe String -> -- ^ The base 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)
+allocateDebugNamesM base ds tps =
+  do ppi <- permGetPPInfo
+     let (strs, ppi') = allocateDebugNames base ds tps ppi
+     gmodify $ \st -> st { stPPInfo = ppi' }
+     return strs
 
 -- | Emit debugging output at the given 'DebugLevel'
 stmtDebugM :: DebugLevel -> (PPInfo -> Doc ()) ->
@@ -2315,16 +2376,6 @@ stmtVerbTraceM :: (PPInfo -> Doc ()) ->
                   PermCheckM ext cblocks blocks tops ret r ps r ps String
 stmtVerbTraceM = stmtDebugM verboseDebugLevel
 
--- | Failure in the statement permission-checking monad
-stmtFailM :: (PPInfo -> Doc ()) -> PermCheckM ext cblocks blocks tops rets r1 ps1
-             (TypedStmtSeq ext blocks tops rets 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)
-
 -- | FIXME HERE: Make 'ImplM' quantify over any underlying monad, so that we do
 -- not have to use 'traversePermImpl' after we run an 'ImplM'
 data WithImplState vars a ps ps' =
@@ -2588,9 +2639,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
@@ -2646,10 +2696,12 @@ emitStmt ::
   StmtPermCheckM ext cblocks blocks tops rets ps_out ps_in
     (RAssign Name stmt_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
+  allocateDebugNamesM Nothing names tps >>>= \debugs ->
+  startNamedBinding debugs (fmap (TypedConsStmt loc stmt pxys)
+                            . strongMbMNamed) >>>= \ns ->
+  modify (\st -> st { stPPInfo = ppInfoApplyAllocation ns debugs (stPPInfo st)}) >>>
+  setVarTypes ns tps >>>
   gmodify (modifySTCurPerms (applyTypedStmt stmt ns)) >>>
   gets (view distPerms . stCurPerms) >>>= \perms_out ->
   stmtVerbTraceM (\i ->
@@ -3080,7 +3132,7 @@ tcEmitStmt' ctx loc (CallHandle _ret freg_untyped _args_ctx args_untyped) =
       _ -> pure []) >>>= \maybe_fun_perms ->
   (stmtEmbedImplM $ foldr1WithDefault (implCatchM "tcEmitStmt (fun perm)" $
                                        typedRegVar freg)
-   (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 ->
@@ -3106,7 +3158,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"
@@ -3132,8 +3184,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
@@ -3238,15 +3291,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 $
@@ -3262,7 +3316,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
 
 
 
@@ -3445,14 +3499,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 _ _) =
@@ -3483,7 +3538,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) =
@@ -3515,7 +3570,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) =
@@ -3528,8 +3583,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) =
@@ -3690,9 +3744,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
@@ -4122,7 +4177,7 @@ tcBlockEntryBody ::
   Block ext cblocks ret args ->
   TypedEntry TCPhase ext blocks tops (gouts :> ret) (CtxToRList args) ghosts ->
   TopPermCheckM ext cblocks blocks tops (gouts :> ret)
-    (Mb ((tops :++: CtxToRList args) :++: ghosts)
+    (NamedMb ((tops :++: CtxToRList args) :++: ghosts)
       (TypedStmtSeq ext blocks tops (gouts :> ret)
        ((tops :++: CtxToRList args) :++: ghosts)))
 tcBlockEntryBody names blk entry@(TypedEntry {..}) =
@@ -4146,6 +4201,9 @@ tcBlockEntryBody names blk entry@(TypedEntry {..}) =
   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
@@ -4159,7 +4217,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 ns = RL.append tops_ns args_ns
       perms_out =
@@ -4219,12 +4277,14 @@ widenEntry dlevel env (TypedEntry {..}) =
   debugTraceTraceLvl dlevel ("Widening entrypoint: " ++ show typedEntryID) $
   case foldl1' (widen dlevel env 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
@@ -4277,7 +4337,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
@@ -4368,3 +4429,82 @@ tcCFG w env endianness dlevel 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)
+
+-- | 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 fb754319e2..8b3b40db8d 100644
--- a/src/SAWScript/HeapsterBuiltins.hs
+++ b/src/SAWScript/HeapsterBuiltins.hs
@@ -54,6 +54,7 @@ module SAWScript.HeapsterBuiltins
        , heapster_print_fun_trans
        , heapster_export_coq
        , heapster_parse_test
+       , heapster_dump_ide_info
        , heapster_set_debug_level
        , heapster_set_translation_checks
        ) where
@@ -124,6 +125,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 Verifier.SAW.Heapster.LLVMGlobalConst
 
 import SAWScript.Prover.Exporter
@@ -304,12 +306,14 @@ mkHeapsterEnv dlevel saw_mod_name llvm_mods@(Some first_mod:_) =
      env_ref <- liftIO $ newIORef env
      dlevel_ref <- liftIO $ newIORef dlevel
      checks_ref <- liftIO $ newIORef doChecks
+     tcfg_ref <- liftIO $ newIORef []
      return $ HeapsterEnv {
        heapsterEnvSAWModule = saw_mod_name,
        heapsterEnvPermEnvRef = env_ref,
        heapsterEnvLLVMModules = llvm_mods,
        heapsterEnvDebugLevel = dlevel_ref,
-       heapsterEnvChecksFlag = checks_ref
+       heapsterEnvChecksFlag = checks_ref,
+       heapsterEnvTCFGs = tcfg_ref
        }
 mkHeapsterEnv _ _ [] = fail "mkHeapsterEnv: empty list of LLVM modules!"
 
@@ -390,8 +394,6 @@ heapster_init_env_for_files_debug _bic _opts mod_filename llvm_filenames =
   heapster_init_env_for_files_gen _bic _opts traceDebugLevel
                                   mod_filename llvm_filenames
 
-
-
 -- | Look up the CFG associated with a symbol name in a Heapster environment
 heapster_get_cfg :: BuiltinContext -> Options -> HeapsterEnv ->
                     String -> TopLevel SAW_CFG
@@ -432,7 +434,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
@@ -1132,7 +1134,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 ->
@@ -1176,11 +1178,12 @@ heapster_typecheck_mut_funs_rename _bic _opts henv fn_names_and_perms =
      env <- liftIO $ readIORef $ heapsterEnvPermEnvRef henv
      sc <- getSharedContext
      let saw_modname = heapsterEnvSAWModule henv
-     env' <- liftIO $
+     (env', tcfgs) <- liftIO $
        let ?ptrWidth = w in
        tcTranslateAddCFGs sc saw_modname env checks endianness dlevel
        some_cfgs_and_perms
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
+     liftIO $ modifyIORef (heapsterEnvTCFGs henv) (\old -> map Some tcfgs ++ old)
 
 
 heapster_typecheck_fun :: BuiltinContext -> Options -> HeapsterEnv ->
@@ -1198,7 +1201,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 ()
@@ -1267,3 +1270,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 f2e4a8bd73..e4cb1dede8 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -4160,6 +4160,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 5da9c83644..d7c018d980 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -116,7 +116,7 @@ import           Lang.Crucible.LLVM.ArraySizeProfile
 import           What4.ProgramLoc (ProgramLoc(..))
 
 import Verifier.SAW.Heapster.Permissions
-import Verifier.SAW.Heapster.SAWTranslation (ChecksFlag)
+import Verifier.SAW.Heapster.SAWTranslation (ChecksFlag,SomeTypedCFG(..))
 
 -- Values ----------------------------------------------------------------------
 
@@ -195,6 +195,8 @@ data HeapsterEnv = HeapsterEnv {
   -- ^ The current permissions environment
   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
   heapsterEnvDebugLevel :: IORef DebugLevel,
   -- ^ The current debug level
   heapsterEnvChecksFlag :: IORef ChecksFlag