diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
index af5d228ecd..11ecf9fbdc 100644
--- a/booster/library/Booster/JsonRpc.hs
+++ b/booster/library/Booster/JsonRpc.hs
@@ -103,14 +103,14 @@ respond stateVar =
             | isJust req.stepTimeout -> pure $ Left $ RpcError.unsupportedOption ("step-timeout" :: String)
             | isJust req.movingAverageStepTimeout ->
                 pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String)
-        RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "execute" $ do
+        RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxExecute $ do
             start <- liftIO $ getTime Monotonic
             -- internalise given constrained term
             let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term
 
             case internalised of
                 Left patternError -> do
-                    void $ Booster.Log.withContext "internalise" $ logPatternError patternError
+                    void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
                     pure $
                         Left $
                             RpcError.backendError $
@@ -152,7 +152,7 @@ respond stateVar =
                                         fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
                                 else Nothing
                     pure $ execResponse duration req result substitution unsupported
-        RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext "add-module" $ runExceptT $ do
+        RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
             -- block other request executions while modifying the server state
             state <- liftIO $ takeMVar stateVar
             let nameAsId = fromMaybe False nameAsId'
@@ -213,7 +213,7 @@ respond stateVar =
                 Booster.Log.logMessage $
                     "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
                 pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash
-        RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "simplify" $ do
+        RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxSimplify $ do
             start <- liftIO $ getTime Monotonic
             let internalised =
                     runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -228,7 +228,7 @@ respond stateVar =
             result <- case internalised of
                 Left patternErrors -> do
                     forM_ patternErrors $ \patternError ->
-                        void $ Booster.Log.withContext "internalise" $ logPatternError patternError
+                        void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
                     pure $
                         Left $
                             RpcError.backendError $
@@ -273,7 +273,7 @@ respond stateVar =
                                 logMessage ("ignoring unsupported predicate parts" :: Text)
                         -- apply the given substitution before doing anything else
                         let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
-                        withContext "constraint" $
+                        withContext CtxConstraint $
                             ApplyEquations.simplifyConstraints
                                 def
                                 mLlvmLibrary
@@ -305,7 +305,7 @@ respond stateVar =
             pure $ second mkSimplifyResponse result
         RpcTypes.GetModel req -> withModule req._module $ \case
             (_, _, Nothing) -> do
-                withContext "get-model" $
+                withContext CtxGetModel $
                     logMessage' ("get-model request, not supported without SMT solver" :: Text)
                 pure $ Left RpcError.notImplemented
             (def, _, Just smtOptions) -> do
@@ -315,7 +315,7 @@ respond stateVar =
                 case internalised of
                     Left patternErrors -> do
                         forM_ patternErrors $ \patternError ->
-                            void $ Booster.Log.withContext "internalise" $ logPatternError patternError
+                            void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
                         pure $
                             Left $
                                 RpcError.backendError $
@@ -327,20 +327,20 @@ respond stateVar =
                         (boolPs, suppliedSubst) <-
                             case things of
                                 TermAndPredicates pat substitution unsupported -> do
-                                    withContext "get-model" $
+                                    withContext CtxGetModel $
                                         logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
 
                                     unless (null unsupported) $ do
-                                        withContext "get-model" $ do
+                                        withContext CtxGetModel $ do
                                             logMessage' ("ignoring unsupported predicates" :: Text)
-                                            withContext "detail" $
+                                            withContext CtxDetail $
                                                 logMessage (Text.unwords $ map prettyPattern unsupported)
                                     pure (Set.toList pat.constraints, substitution)
                                 Predicates ps -> do
                                     unless (null ps.ceilPredicates && null ps.unsupported) $ do
-                                        withContext "get-model" $ do
+                                        withContext CtxGetModel $ do
                                             logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text)
-                                            withContext "detail" $
+                                            withContext CtxDetail $
                                                 logMessage
                                                     ( Text.unlines $
                                                         map
@@ -354,8 +354,8 @@ respond stateVar =
                             if null boolPs && Map.null suppliedSubst
                                 then do
                                     -- as per spec, no predicate, no answer
-                                    withContext "get-model" $
-                                        withContext "smt" $
+                                    withContext CtxGetModel $
+                                        withContext CtxSMT $
                                             logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
                                     pure $ Left SMT.Unknown
                                 else do
@@ -365,8 +365,8 @@ respond stateVar =
                                     case result of
                                         Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors
                                         Right response -> pure response
-                        withContext "get-model" $
-                            withContext "smt" $
+                        withContext CtxGetModel $
+                            withContext CtxSMT $
                                 logMessage $
                                     "SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
                         pure . Right . RpcTypes.GetModel $ case smtResult of
@@ -413,14 +413,14 @@ respond stateVar =
                                         { satisfiable = RpcTypes.Sat
                                         , substitution
                                         }
-        RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "implies" $ do
+        RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxImplies $ do
             -- internalise given constrained term
             let internalised =
                     runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials
 
             case (internalised req.antecedent.term, internalised req.consequent.term) of
                 (Left patternError, _) -> do
-                    void $ Booster.Log.withContext "internalise" $ logPatternError patternError
+                    void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
                     pure $
                         Left $
                             RpcError.backendError $
@@ -428,7 +428,7 @@ respond stateVar =
                                     [ patternErrorToRpcError patternError
                                     ]
                 (_, Left patternError) -> do
-                    void $ Booster.Log.withContext "internalise" $ logPatternError patternError
+                    void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
                     pure $
                         Left $
                             RpcError.backendError $
@@ -440,11 +440,11 @@ respond stateVar =
                         logMessage'
                             ("aborting due to unsupported predicate parts" :: Text)
                         unless (null unsupportedL) $
-                            withContext "detail" $
+                            withContext CtxDetail $
                                 logMessage
                                     (Text.unwords $ map prettyPattern unsupportedL)
                         unless (null unsupportedR) $
-                            withContext "detail" $
+                            withContext CtxDetail $
                                 logMessage
                                     (Text.unwords $ map prettyPattern unsupportedR)
                     let
diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index b6b96d6d02..82204a97e6 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -1,9 +1,31 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Booster.Log (module Booster.Log) where
+module Booster.Log (
+    ContextFor (..),
+    LogMessage (..),
+    Logger (..),
+    LoggerT (..),
+    LoggerMIO (..),
+    ToLogFormat (..),
+    WithJsonMessage (..),
+    logMessage,
+    logMessage',
+    logPretty,
+    filterLogger,
+    jsonLogger,
+    textLogger,
+    withContext,
+    withKorePatternContext,
+    withPatternContext,
+    withRuleContext,
+    withTermContext,
+    -- re-export SimpleContext for withContext
+    SimpleContext (..),
+) where
 
 import Control.Monad (when)
 import Control.Monad.IO.Class
@@ -16,26 +38,25 @@ import Control.Monad.Trans.State (StateT (..))
 import Control.Monad.Trans.State.Strict qualified as Strict
 import Data.Aeson (ToJSON (..), Value (..), (.=))
 import Data.Aeson.Encode.Pretty (Config (confIndent), Indent (Spaces), encodePretty')
-import Data.Aeson.Key qualified as Key
 import Data.Aeson.Types (object)
 import Data.Coerce (coerce)
-import Data.Data (Proxy (..))
 import Data.Hashable qualified
 import Data.List (foldl', intercalate, intersperse)
 import Data.List.Extra (splitOn, takeEnd)
+import Data.Maybe (fromMaybe)
 import Data.Set qualified as Set
-import Data.String (IsString)
 import Data.Text (Text, pack)
-import Data.Text.Lazy qualified as LazyText
-import GHC.Exts (IsString (..))
-import GHC.TypeLits (KnownSymbol, symbolVal)
+import Data.Text.Encoding (decodeUtf8)
 import Prettyprinter (Pretty, pretty)
+import System.Log.FastLogger (FormattedTime)
+import UnliftIO (MonadUnliftIO)
 
 import Booster.Definition.Attributes.Base
 import Booster.Definition.Base (RewriteRule (..), SourceRef (..), sourceRef)
 import Booster.Pattern.Base (
     Pattern (..),
     Predicate (..),
+    Symbol (..),
     Term (..),
     TermAttributes (hash),
     pattern AndTerm,
@@ -44,11 +65,9 @@ import Booster.Prettyprinter (renderOneLineText)
 import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
 import Booster.Syntax.Json.Externalise (externaliseTerm)
 import Booster.Util (Flag (..))
-import Data.Text.Encoding (decodeUtf8)
 import Kore.JsonRpc.Types (rpcJsonConfig)
-import Kore.Util (showHashHex)
-import System.Log.FastLogger (FormattedTime)
-import UnliftIO (MonadUnliftIO)
+import Kore.JsonRpc.Types.ContextLog as CL
+import Kore.Util
 
 newtype Logger a = Logger (a -> IO ())
 
@@ -56,13 +75,32 @@ class ToLogFormat a where
     toTextualLog :: a -> Text
     toJSONLog :: a -> Value
 
-data LogContext = forall a. ToLogFormat a => LogContext a
+instance ToLogFormat CLContext where
+    toTextualLog = pack . show
+    toJSONLog = toJSON
+
+instance ToLogFormat Text where
+    toTextualLog t = t
+    toJSONLog t = String t
+
+instance ToLogFormat Term where
+    toTextualLog t = renderOneLineText $ pretty t
+    toJSONLog t = toJSON $ addHeader $ externaliseTerm t
 
-instance IsString LogContext where
-    fromString = LogContext . pack
+instance ToLogFormat (RewriteRule tag) where
+    toTextualLog = shortRuleLocation
+    toJSONLog = String . shortRuleLocation
+
+shortRuleLocation :: RewriteRule tag -> Text
+shortRuleLocation rule = renderOneLineText $
+    pretty $
+        case sourceRef rule of
+            Located l@Location{file = FileSource f} ->
+                Located l{file = FileSource $ "..." <> (intercalate "/" $ takeEnd 3 $ splitOn "/" f)}
+            loc -> loc
 
 data LogMessage where
-    LogMessage :: ToLogFormat a => Flag "alwaysShown" -> [LogContext] -> a -> LogMessage
+    LogMessage :: ToLogFormat a => Flag "alwaysShown" -> [CLContext] -> a -> LogMessage
 
 class MonadIO m => LoggerMIO m where
     getLogger :: m (Logger LogMessage)
@@ -100,78 +138,84 @@ logMessage' a =
 logPretty :: (LoggerMIO m, Pretty a) => a -> m ()
 logPretty = logMessage . renderOneLineText . pretty
 
-withContext :: LoggerMIO m => LogContext -> m a -> m a
-withContext c =
+withContext :: LoggerMIO m => SimpleContext -> m a -> m a
+withContext c = withContext_ (CLNullary c)
+
+withContext_ :: LoggerMIO m => CLContext -> m a -> m a
+withContext_ c =
     withLogger
         ( \(Logger l) -> Logger $ l . (\(LogMessage alwaysShown ctxt m) -> LogMessage alwaysShown (c : ctxt) m)
         )
 
-newtype TermCtxt = TermCtxt Int
-
-instance ToLogFormat TermCtxt where
-    toTextualLog (TermCtxt hsh) = "term " <> (showHashHex hsh)
-    toJSONLog (TermCtxt hsh) = object ["term" .= showHashHex hsh]
-
-newtype HookCtxt = HookCtxt Text
-
-instance ToLogFormat HookCtxt where
-    toTextualLog (HookCtxt h) = "hook " <> h
-    toJSONLog (HookCtxt h) = object ["hook" .= h]
-
-instance ToLogFormat Term where
-    toTextualLog t = renderOneLineText $ pretty t
-    toJSONLog t = toJSON $ addHeader $ externaliseTerm t
-
-instance ToLogFormat Text where
-    toTextualLog t = t
-    toJSONLog t = String t
-
 withTermContext :: LoggerMIO m => Term -> m a -> m a
-withTermContext t@(Term attrs _) m = withContext (LogContext $ TermCtxt attrs.hash) $ do
-    withContext "kore-term" $ logMessage t
-    m
+withTermContext t@(Term attrs _) m =
+    withContext_ (CLWithId . CtxTerm . ShortId $ showHashHex attrs.hash) $ do
+        withContext CtxKoreTerm $ logMessage t
+        m
 
 withPatternContext :: LoggerMIO m => Pattern -> m a -> m a
 withPatternContext Pattern{term, constraints} m =
-    let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints
+    let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME
      in withTermContext t' m
 
 instance ToLogFormat KorePattern where
     toTextualLog = prettyPattern
     toJSONLog p = toJSON p
 
-newtype KorePatternCtxt = KorePatternCtxt KorePattern
-
-instance ToLogFormat KorePatternCtxt where
-    toTextualLog (KorePatternCtxt t) = "term " <> (showHashHex $ Data.Hashable.hash $ prettyPattern t)
-    toJSONLog (KorePatternCtxt t) = object ["term" .= (showHashHex $ Data.Hashable.hash $ prettyPattern t)]
-
-instance KnownSymbol k => ToLogFormat (RewriteRule k) where
-    toTextualLog RewriteRule{attributes} =
-        LazyText.toStrict $
-            (LazyText.toLower $ LazyText.pack $ symbolVal (Proxy :: Proxy k))
-                <> " "
-                <> (LazyText.take 7 . LazyText.fromStrict . coerce $ attributes.uniqueId)
-    toJSONLog RewriteRule{attributes} =
-        object
-            [ (Key.fromText $ LazyText.toStrict $ LazyText.toLower $ LazyText.pack $ symbolVal (Proxy :: Proxy k))
-                .= (coerce attributes.uniqueId :: Text)
-            ]
-
 withKorePatternContext :: LoggerMIO m => KorePattern -> m a -> m a
-withKorePatternContext t m = withContext (LogContext $ KorePatternCtxt t) $ do
-    withContext "kore-term" $ logMessage t
-    m
-
-withRuleContext :: KnownSymbol tag => LoggerMIO m => RewriteRule tag -> m a -> m a
-withRuleContext rule m = withContext (LogContext rule) $ do
-    withContext "detail" $ logPretty $ case sourceRef rule of
+withKorePatternContext p m =
+    withContextFor p $ do
+        withContext CtxKoreTerm $ logMessage p
+        m
+
+withRuleContext ::
+    ContextFor (RewriteRule tag) =>
+    LoggerMIO m =>
+    RewriteRule tag ->
+    m a ->
+    m a
+withRuleContext rule m = withContextFor rule $ do
+    withContext CtxDetail $ logPretty $ case sourceRef rule of
         Located Location{file = FileSource f, position} ->
             Located
                 Location{file = FileSource $ "..." <> (intercalate "/" $ takeEnd 3 $ splitOn "/" f), position}
         loc -> loc
     m
 
+class ContextFor a where
+    withContextFor :: LoggerMIO m => a -> m b -> m b
+
+instance ContextFor Term where
+    withContextFor (Term attrs _) =
+        withContext_ (CLWithId . CtxTerm . ShortId $ showHashHex attrs.hash)
+
+instance ContextFor KorePattern where
+    withContextFor p =
+        withContext_ (CLWithId . CtxTerm . ShortId . showHashHex . Data.Hashable.hash $ show p) -- FIXME
+
+instance ContextFor (RewriteRule "Rewrite") where
+    withContextFor r =
+        withContext_ (CLWithId . CtxRewrite $ parseRuleId r)
+
+instance ContextFor (RewriteRule "Function") where
+    withContextFor r =
+        withContext_ (CLWithId . CtxFunction $ parseRuleId r)
+
+instance ContextFor (RewriteRule "Simplification") where
+    withContextFor r =
+        withContext_ (CLWithId . CtxSimplification $ parseRuleId r)
+
+instance ContextFor (RewriteRule "Ceil") where
+    withContextFor r =
+        withContext_ (CLWithId . CtxCeil $ parseRuleId r)
+
+instance ContextFor Symbol where
+    withContextFor s =
+        withContext_ (CLWithId . CtxHook $ maybe "not-hooked" decodeUtf8 s.attributes.hook)
+
+parseRuleId :: RewriteRule tag -> CL.UniqueId
+parseRuleId = fromMaybe CL.UNKNOWN . CL.parseUId . coerce . (.attributes.uniqueId)
+
 data WithJsonMessage where
     WithJsonMessage :: ToLogFormat a => Value -> a -> WithJsonMessage
 
@@ -196,7 +240,7 @@ instance MonadIO m => LoggerMIO (LoggerT m) where
 
 textLogger :: ((Maybe FormattedTime -> Control.Monad.Logger.LogStr) -> IO ()) -> Logger LogMessage
 textLogger l = Logger $ \(LogMessage _ ctxts msg) ->
-    let logLevel = mconcat $ intersperse "][" $ map (\(LogContext lc) -> toTextualLog lc) ctxts
+    let logLevel = mconcat $ intersperse "][" $ map toTextualLog ctxts
      in l $ \mTime ->
             ( case mTime of
                 Nothing -> mempty
@@ -210,7 +254,7 @@ textLogger l = Logger $ \(LogMessage _ ctxts msg) ->
 
 jsonLogger :: ((Maybe FormattedTime -> Control.Monad.Logger.LogStr) -> IO ()) -> Logger LogMessage
 jsonLogger l = Logger $ \(LogMessage _ ctxts msg) ->
-    let ctxt = toJSON $ map (\(LogContext lc) -> toJSONLog lc) ctxts
+    let ctxt = toJSON $ map toJSONLog ctxts
      in liftIO $
             l $ \mTime ->
                 ( Control.Monad.Logger.toLogStr $
diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index 8c110f003b..367bf8e26f 100644
--- a/booster/library/Booster/Pattern/ApplyEquations.hs
+++ b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 {- |
@@ -48,7 +49,6 @@ import Data.Set qualified as Set
 import Data.Text (Text)
 import Data.Text qualified as Text
 import Data.Text.Encoding qualified as Text
-import GHC.TypeLits (KnownSymbol)
 import Prettyprinter
 
 import Booster.Builtin as Builtin
@@ -218,7 +218,7 @@ popRecursion = do
     s <- getState
     if null s.recursionStack
         then do
-            withContext "abort" $
+            withContext CtxAbort $
                 logMessage ("Trying to pop an empty recursion stack" :: Text)
             throw $ InternalError "Trying to pop an empty recursion stack"
         else eqState $ put s{recursionStack = tail s.recursionStack}
@@ -239,16 +239,16 @@ fromCache tag t = eqState $ Map.lookup t <$> gets (select tag . (.cache))
 
 logWarn :: LoggerMIO m => Text -> m ()
 logWarn msg =
-    withContext "warning" $
+    withContext CtxWarn $
         logMessage msg
 
 checkForLoop :: LoggerMIO io => Term -> EquationT io ()
 checkForLoop t = do
     EquationState{termStack} <- getState
     whenJust (Seq.elemIndexL t termStack) $ \i -> do
-        withContext "abort" $ do
+        withContext CtxAbort $ do
             logWarn "Equation loop detected."
-            withContext "detail" $
+            withContext CtxDetail $
                 logMessage $
                     renderOneLineText $
                         hsep
@@ -304,7 +304,7 @@ iterateEquations direction preference startTerm = do
     checkCounter counter = do
         config <- getConfig
         when (counter > config.maxRecursion) $ do
-            withContext "abort" $ do
+            withContext CtxAbort $ do
                 logWarn
                     "Recursion limit exceeded. The limit can be increased by \
                     \ restarting the server with '--equation-max-recursion N'."
@@ -317,11 +317,11 @@ iterateEquations direction preference startTerm = do
             config <- getConfig
             currentCount <- countSteps
             when (coerce currentCount > config.maxIterations) $ do
-                withContext "abort" $ do
+                withContext CtxAbort $ do
                     logWarn $
                         renderOneLineText $
                             "Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
-                    withContext "detail" . logMessage . renderOneLineText $
+                    withContext CtxDetail . logMessage . renderOneLineText $
                         "Final term:" <+> pretty currentTerm
                 throw $
                     TooManyIterations currentCount startTerm currentTerm
@@ -351,18 +351,18 @@ llvmSimplify term = do
   where
     evalLlvm definition api cb t@(Term attributes _)
         | attributes.isEvaluated = pure t
-        | isConcrete t && attributes.canBeEvaluated = withContext "llvm" $ do
+        | isConcrete t && attributes.canBeEvaluated = withContext CtxLlvm $ do
             LLVM.simplifyTerm api definition t (sortOfTerm t)
                 >>= \case
                     Left (LlvmError e) -> do
-                        withContext "abort" $
+                        withContext CtxAbort $
                             logWarn $
                                 "LLVM backend error detected: " <> Text.decodeUtf8 e
                         throw $ UndefinedTerm t $ LlvmError e
                     Right result -> do
                         when (result /= t) $ do
                             setChanged
-                            withContext "success" $
+                            withContext CtxSuccess $
                                 withTermContext result $
                                     pure ()
                         pure result
@@ -531,8 +531,8 @@ cached cacheTag cb t@(Term attributes _)
             Just cachedTerm -> do
                 when (t /= cachedTerm) $ do
                     setChanged
-                    withContext "success" $
-                        withContext "cached" $
+                    withContext CtxSuccess $
+                        withContext CtxCached $
                             withTermContext cachedTerm $
                                 pure ()
                 pure cachedTerm
@@ -563,12 +563,11 @@ applyHooksAndEquations pref term = do
         case term of
             SymbolApplication sym _sorts args
                 | Just hook <- flip Map.lookup Builtin.hooks =<< sym.attributes.hook -> do
-                    let hookName = maybe "UNKNOWN" Text.decodeUtf8 sym.attributes.hook
-                        onError e = do
-                            withContext "abort" $
+                    let onError e = do
+                            withContext CtxAbort $
                                 logWarn e
                             throw (InternalError e)
-                    withContext (LogContext $ HookCtxt hookName) $
+                    withContextFor sym $
                         either onError checkChanged $
                             runExcept (hook args)
             _other -> pure Nothing
@@ -577,9 +576,9 @@ applyHooksAndEquations pref term = do
     -- cannot blindly set the changed flag when we have applied a hook
     checkChanged :: Maybe Term -> EquationT io (Maybe Term)
     checkChanged Nothing =
-        withContext "failure" (logMessage ("Hook returned no result" :: Text)) >> pure Nothing
+        withContext CtxFailure (logMessage ("Hook returned no result" :: Text)) >> pure Nothing
     checkChanged (Just t) =
-        withContext "success" $ withTermContext t $ do
+        withContext CtxSuccess $ withTermContext t $ do
             unless (t == term) setChanged
             pure (Just t)
 
@@ -621,7 +620,7 @@ handleFunctionEquation continue abort = \case
     IndeterminateCondition{} -> abort
     ConditionFalse _ -> continue
     EnsuresFalse p -> do
-        withContext "abort" $
+        withContext CtxAbort $
             logMessage ("A side condition was found to be false during evaluation (pruning)" :: Text)
         throw $ SideConditionFalse p
     RuleNotPreservingDefinedness -> abort
@@ -634,7 +633,7 @@ handleSimplificationEquation continue _abort = \case
     IndeterminateCondition{} -> continue
     ConditionFalse _ -> continue
     EnsuresFalse p -> do
-        withContext "abort" $
+        withContext CtxAbort $
             logMessage ("A side condition was found to be false during evaluation (pruning)" :: Text)
         throw $ SideConditionFalse p
     RuleNotPreservingDefinedness -> continue
@@ -642,7 +641,7 @@ handleSimplificationEquation continue _abort = \case
 
 applyEquations ::
     forall io tag.
-    KnownSymbol tag =>
+    ContextFor (RewriteRule tag) =>
     LoggerMIO io =>
     Theory (RewriteRule tag) ->
     ResultHandler io ->
@@ -651,7 +650,7 @@ applyEquations ::
 applyEquations theory handler term = do
     let index = Idx.termTopIndex term
     when (Idx.hasNone index) $ do
-        withContext "abort" $ logMessage ("Index 'None'" :: Text)
+        withContext CtxAbort $ logMessage ("Index 'None'" :: Text)
         throw (IndexIsNone term)
     let
         indexes = Set.toList $ Idx.coveringIndexes index
@@ -679,18 +678,18 @@ applyEquations theory handler term = do
         pure term -- nothing to do, term stays the same
     processEquations (eq : rest) = do
         withRuleContext eq (applyEquation term eq) >>= \case
-            Right t -> setChanged >> (withContext (LogContext eq) $ withContext "success" $ withTermContext t $ pure t)
+            Right t -> setChanged >> (withContextFor eq $ withContext CtxSuccess $ withTermContext t $ pure t)
             Left (m, err) ->
                 handler
-                    ( ( withContext (LogContext eq) $
+                    ( ( withContextFor eq $
                             m $
-                                withContext "failure" . withContext "continue"
+                                withContext CtxFailure . withContext CtxContinue
                       )
                         >> processEquations rest
                     )
-                    ( ( withContext (LogContext eq) $
+                    ( ( withContextFor eq $
                             m $
-                                withContext "failure" . withContext "break"
+                                withContext CtxFailure . withContext CtxBreak
                       )
                         >> pure term
                     )
@@ -698,7 +697,6 @@ applyEquations theory handler term = do
 
 applyEquation ::
     forall io tag.
-    KnownSymbol tag =>
     LoggerMIO io =>
     Term ->
     RewriteRule tag ->
@@ -708,7 +706,7 @@ applyEquation ::
 applyEquation term rule = runExceptT $ do
     -- ensured by internalisation: no existentials in equations
     unless (null rule.existentials) $ do
-        withContext "abort" $
+        withContext CtxAbort $
             logMessage ("Equation with existentials" :: Text)
         lift . throw . InternalError $
             "Equation with existentials: " <> Text.pack (show rule)
@@ -735,7 +733,7 @@ applyEquation term rule = runExceptT $ do
         MatchFailed failReason ->
             throwE
                 ( \ctxt ->
-                    withContext "match" $
+                    withContext CtxMatch $
                         ctxt $
                             logPretty failReason
                 , FailedMatch failReason
@@ -743,7 +741,7 @@ applyEquation term rule = runExceptT $ do
         MatchIndeterminate remainder ->
             throwE
                 ( \ctxt ->
-                    withContext "match" $
+                    withContext CtxMatch $
                         ctxt $
                             logMessage $
                                 WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $
@@ -756,11 +754,11 @@ applyEquation term rule = runExceptT $ do
             -- forall (v, t) : subst. concrete(v) -> isConstructorLike(t) /\
             --                        symbolic(v) -> not $ t isConstructorLike(t)
             -- is violated
-            withContext "match" $ checkConcreteness rule.attributes.concreteness subst
+            withContext CtxMatch $ checkConcreteness rule.attributes.concreteness subst
 
-            withContext "match" $ withContext "success" $ do
+            withContext CtxMatch $ withContext CtxSuccess $ do
                 logMessage rule
-                withContext "substitution"
+                withContext CtxSubstitution
                     $ logMessage
                     $ WithJsonMessage
                         (object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList subst)])
@@ -829,7 +827,7 @@ applyEquation term rule = runExceptT $ do
     -- Simplify given predicate in a nested EquationT execution.
     -- Call 'whenBottom' if it is Bottom, return Nothing if it is Top,
     -- otherwise return the simplified remaining predicate.
-    checkConstraint whenBottom (Predicate p) = withContext "constraint" $ do
+    checkConstraint whenBottom (Predicate p) = withContext CtxConstraint $ do
         let fallBackToUnsimplifiedOrBottom :: EquationFailure -> EquationT io Term
             fallBackToUnsimplifiedOrBottom = \case
                 UndefinedTerm{} -> pure FalseBool
@@ -947,10 +945,10 @@ simplifyConstraint' recurseIntoEvalBool = \case
             mbApi <- (.llvmApi) <$> getConfig
             case mbApi of
                 Just api ->
-                    withContext "llvm" $
+                    withContext CtxLlvm $
                         LLVM.simplifyBool api t >>= \case
                             Left (LlvmError e) -> do
-                                withContext "abort" $
+                                withContext CtxAbort $
                                     logWarn $
                                         "LLVM backend error detected: " <> Text.decodeUtf8 e
                                 throw $ UndefinedTerm t $ LlvmError e
@@ -959,7 +957,7 @@ simplifyConstraint' recurseIntoEvalBool = \case
                                         if res
                                             then TrueBool
                                             else FalseBool
-                                withContext "success" $
+                                withContext CtxSuccess $
                                     withTermContext result $
                                         pure result
                 Nothing -> if recurseIntoEvalBool then evalBool t else pure t
diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
index 7b2349849b..ba37452c53 100644
--- a/booster/library/Booster/Pattern/Rewrite.hs
+++ b/booster/library/Booster/Pattern/Rewrite.hs
@@ -44,17 +44,7 @@ import Prettyprinter
 import Booster.Definition.Attributes.Base
 import Booster.Definition.Base
 import Booster.LLVM as LLVM (API)
-import Booster.Log (
-    LogMessage,
-    Logger,
-    LoggerMIO (..),
-    WithJsonMessage (..),
-    logMessage,
-    logPretty,
-    withContext,
-    withPatternContext,
-    withRuleContext,
- )
+import Booster.Log
 import Booster.Pattern.ApplyEquations (
     EquationFailure (..),
     SimplifierCache,
@@ -282,27 +272,27 @@ applyRule ::
 applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRuleAppT $ do
     def <- lift getDefinition
     -- unify terms
-    subst <- withContext "match" $ case matchTerms Rewrite def rule.lhs pat.term of
+    subst <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of
         MatchFailed (SubsortingError sortError) -> do
-            withContext "error" $ logPretty sortError
+            withContext CtxError $ logPretty sortError
             failRewrite $ RewriteSortError rule pat.term sortError
         MatchFailed err@ArgLengthsDiffer{} -> do
-            withContext "error" $ logPretty err
+            withContext CtxError $ logPretty err
             failRewrite $ InternalMatchError $ renderText $ pretty err
         MatchFailed reason -> do
-            withContext "failure" $ logPretty reason
+            withContext CtxFailure $ logPretty reason
             fail "Rule matching failed"
         MatchIndeterminate remainder -> do
-            withContext "indeterminate" $
+            withContext CtxIndeterminate $
                 logMessage $
                     WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $
                         renderOneLineText $
                             "Uncertain about match with rule. Remainder:" <+> pretty remainder
             failRewrite $ RuleApplicationUnclear rule pat.term remainder
         MatchSuccess substitution -> do
-            withContext "success" $ do
+            withContext CtxSuccess $ do
                 logMessage rule
-                withContext "substitution"
+                withContext CtxSubstitution
                     $ logMessage
                     $ WithJsonMessage
                         ( object
@@ -316,7 +306,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
     -- Also fail the whole rewrite if a rule applies but may introduce
     -- an undefined term.
     unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do
-        withContext "definedness" . withContext "abort" $
+        withContext CtxDefinedness . withContext CtxAbort $
             logMessage $
                 renderOneLineText $
                     "Uncertain about definedness of rule due to:"
@@ -347,7 +337,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
     mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask
 
     let smtUnclear = do
-            withContext "constraint" . withContext "abort" . logMessage . renderOneLineText $
+            withContext CtxConstraint . withContext CtxAbort . logMessage . renderOneLineText $
                 "Uncertain about condition(s) in a rule:" <+> pretty unclearRequires
             failRewrite $
                 RuleConditionUnclear rule . coerce . foldl1 AndTerm $
@@ -364,7 +354,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                     liftIO $ Exception.throw other -- fail hard on other SMT errors
                 Right (Just False) -> do
                     -- requires is actually false given the prior
-                    withContext "failure" $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
+                    withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
                     RewriteRuleAppT $ pure NotApplied
                 Right (Just True) ->
                     pure () -- can proceed
@@ -372,7 +362,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                     smtUnclear -- no implication could be determined
         Nothing ->
             unless (null unclearRequires) $ do
-                withContext "constraint" . withContext "abort" $
+                withContext CtxConstraint . withContext CtxAbort $
                     logMessage $
                         renderOneLineText $
                             "Uncertain about a condition(s) in rule, no SMT solver:" <+> pretty unclearRequires
@@ -392,7 +382,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
     whenJust mbSolver $ \solver ->
         (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
             Right (Just False) -> do
-                withContext "success" $ logMessage ("New constraints evaluated to #Bottom." :: Text)
+                withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
                 RewriteRuleAppT $ pure Trivial
             Right _other ->
                 pure ()
@@ -423,7 +413,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                     <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints)
                 )
                 ceilConditions
-    withContext "success" $
+    withContext CtxSuccess $
         withPatternContext rewritten $
             return (rule, rewritten)
   where
@@ -438,7 +428,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
         RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask
         oldCache <- lift . RewriteT . lift $ get
         (simplified, cache) <-
-            withContext "constraint" $
+            withContext CtxConstraint $
                 simplifyConstraint definition llvmApi smtSolver oldCache p
         -- update cache
         lift . RewriteT . lift . modify $ const cache
@@ -694,7 +684,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
         flip runStateT rewriteStart $ doSteps False pat
     pure (counter, traces, rr)
   where
-    logDepth = withContext "depth" . logMessage
+    logDepth = withContext CtxDepth . logMessage
 
     depthReached n = maybe False (n >=) mbMaxDepth
 
@@ -711,7 +701,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
     updateCache simplifierCache = modify $ \rss -> rss{simplifierCache}
 
     simplifyP :: Pattern -> StateT RewriteStepsState io (Maybe Pattern)
-    simplifyP p = withContext "simplify" $ do
+    simplifyP p = withContext CtxSimplify $ do
         st <- get
         let cache = st.simplifierCache
             smt = st.smtSolver
@@ -853,7 +843,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
                                 withSimplified pat' "Retrying with simplified pattern" (doSteps True)
                             | otherwise -> do
                                 -- was already simplified, emit an abort log entry
-                                withRuleContext rule . withContext "match" . withContext "abort" . logMessage $
+                                withRuleContext rule . withContext CtxMatch . withContext CtxAbort . logMessage $
                                     WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $
                                         renderOneLineText $
                                             "Uncertain about match with rule. Remainder:" <+> pretty remainder
diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs
index b9b9b61140..5d0fd5b0c1 100644
--- a/booster/library/Booster/SMT/Interface.hs
+++ b/booster/library/Booster/SMT/Interface.hs
@@ -82,7 +82,7 @@ declareVariables transState = do
      - set user-specified timeout for queries
 -}
 initSolver :: Log.LoggerMIO io => KoreDefinition -> SMTOptions -> io SMT.SMTContext
-initSolver def smtOptions = Log.withContext "smt" $ do
+initSolver def smtOptions = Log.withContext Log.CtxSMT $ do
     prelude <- translatePrelude def
 
     Log.logMessage ("Starting new SMT solver" :: Text)
@@ -168,13 +168,13 @@ getModelFor ::
     Map Variable Term -> -- supplied substitution
     io (Either SMTError (Either SMT.Response (Map Variable Term)))
 getModelFor ctxt ps subst
-    | null ps && Map.null subst = Log.withContext "smt" $ do
+    | null ps && Map.null subst = Log.withContext Log.CtxSMT $ do
         Log.logMessage ("No constraints or substitutions to check, returning Sat" :: Text)
         pure . Right . Right $ Map.empty
-    | Left errMsg <- translated = Log.withContext "smt" $ do
+    | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do
         Log.logMessage $ "SMT translation error: " <> errMsg
         smtTranslateError errMsg
-    | Right (smtAsserts, transState) <- translated = Log.withContext "smt" $ do
+    | Right (smtAsserts, transState) <- translated = Log.withContext Log.CtxSMT $ do
         evalSMT ctxt . runExceptT $ do
             lift $ hardResetSolver ctxt.options
             solve smtAsserts transState
@@ -330,10 +330,10 @@ checkPredicates ::
     io (Either SMTError (Maybe Bool))
 checkPredicates ctxt givenPs givenSubst psToCheck
     | null psToCheck = pure . Right $ Just True
-    | Left errMsg <- translated = Log.withContext "smt" $ do
-        Log.withContext "abort" $ Log.logMessage $ "SMT translation error: " <> errMsg
+    | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do
+        Log.withContext Log.CtxAbort $ Log.logMessage $ "SMT translation error: " <> errMsg
         pure . Left . SMTTranslationError $ errMsg
-    | Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext "smt" $ do
+    | Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext Log.CtxSMT $ do
         evalSMT ctxt . runExceptT $ do
             lift $ hardResetSolver ctxt.options
             solve smtGiven sexprsToCheck transState
@@ -400,13 +400,13 @@ checkPredicates ctxt givenPs givenSubst psToCheck
     failBecauseUnknown =
         smtRun GetReasonUnknown >>= \case
             ReasonUnknown reason -> do
-                Log.withContext "abort" $
+                Log.withContext Log.CtxAbort $
                     Log.logMessage $
                         "Returned Unknown. Reason: " <> reason
                 throwE $ SMTSolverUnknown reason givenPs psToCheck
             other -> do
                 let msg = "Unexpected result while calling ':reason-unknown': " <> show other
-                Log.withContext "abort" $ Log.logMessage $ Text.pack msg
+                Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg
                 throwSMT' msg
 
     -- Given the known truth and the expressions to check,
diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs
index c64cce9969..b490df12d2 100644
--- a/booster/tools/booster/Proxy.hs
+++ b/booster/tools/booster/Proxy.hs
@@ -35,7 +35,7 @@ import System.Clock (Clock (Monotonic), TimeSpec, diffTimeSpec, getTime, toNanoS
 import Booster.Definition.Base (KoreDefinition)
 import Booster.JsonRpc as Booster (ServerState (..), execStateToKoreJson, toExecState)
 import Booster.JsonRpc.Utils
-import Booster.Log qualified
+import Booster.Log
 import Booster.Syntax.Json.Internalise
 import Kore.Attribute.Symbol (StepperAttributes)
 import Kore.IndexedModule.MetadataTools (SmtMetadataTools)
@@ -111,7 +111,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                     logStats ImpliesM (boosterTime, 0)
                     pure res
                 Left err -> do
-                    Booster.Log.withContext "proxy" $
+                    Booster.Log.withContext CtxProxy $
                         Booster.Log.logMessage' $
                             Text.pack $
                                 "implies error in booster: " <> fromError err
@@ -140,7 +140,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
         (result, kTime) <-
             case bResult of
                 Left err -> do
-                    Booster.Log.withContext "proxy" $
+                    Booster.Log.withContext CtxProxy $
                         Booster.Log.logMessage' $
                             Text.pack $
                                 "get-model error in booster: " <> fromError err
@@ -148,13 +148,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                 Right (GetModel res@GetModelResult{})
                     -- re-check with legacy-kore if result is unknown
                     | Unknown <- res.satisfiable -> do
-                        Booster.Log.withContext "proxy" $
-                            Booster.Log.withContext "abort" $
+                        Booster.Log.withContext CtxProxy $
+                            Booster.Log.withContext CtxAbort $
                                 Booster.Log.logMessage $
                                     Text.pack "Re-checking a get-model result Unknown"
                         r@(kResult, _) <- Stats.timed $ kore req
-                        Booster.Log.withContext "proxy" $
-                            Booster.Log.withContext "abort" $
+                        Booster.Log.withContext CtxProxy $
+                            Booster.Log.withContext CtxAbort $
                                 Booster.Log.logMessage $
                                     "Double-check returned " <> toStrict (encodeToLazyText kResult)
                         pure r
@@ -187,9 +187,9 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                         when (koreRes.state /= boosterRes.state) $ do
                             bState <- liftIO (MVar.readMVar boosterState)
 
-                            Booster.Log.withContext "proxy" $
-                                Booster.Log.withContext "abort" $
-                                    Booster.Log.withContext "detail" $
+                            Booster.Log.withContext CtxProxy $
+                                Booster.Log.withContext CtxAbort $
+                                    Booster.Log.withContext CtxDetail $
                                         Booster.Log.logMessage $
                                             let m = fromMaybe bState.defaultMain simplifyReq._module
                                                 def =
@@ -234,7 +234,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                     fromString (String s) = s
                     fromString other = Text.pack (show other)
 
-                Booster.Log.withContext "proxy" $
+                Booster.Log.withContext CtxProxy $
                     Booster.Log.logMessage' $
                         Text.unwords
                             ["Problem with simplify request: ", Text.pack getErrMsg, "-", boosterError]
@@ -244,7 +244,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                 pure . Left $ ErrorObj "Wrong result type" (-32002) $ toJSON _wrong
 
     loggedKore method r = do
-        Booster.Log.withContext "proxy" $
+        Booster.Log.withContext CtxProxy $
             Booster.Log.logMessage' $
                 Text.pack $
                     show method <> " (using kore)"
@@ -255,7 +255,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
     logStats method (time, koreTime)
         | Just v <- statsVar = do
             addStats v method time koreTime
-            Booster.Log.withContext "proxy" $
+            Booster.Log.withContext CtxProxy $
                 Booster.Log.logMessage' $
                     Text.pack $
                         unwords
@@ -305,7 +305,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
         ExecuteRequest ->
         m (Either ErrorObj (API 'Res))
     executionLoop logSettings def (currentDepth@(Depth cDepth), !time, !koreTime, !rpcLogs) r = do
-        Booster.Log.withContext "proxy" $
+        Booster.Log.withContext CtxProxy $
             Booster.Log.logMessage $
                 Text.pack $
                     if currentDepth == 0
@@ -328,7 +328,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                 | DepthBound <- boosterResult.reason
                 , Just forceDepth <- cfg.forceFallback
                 , forceDepth == boosterResult.depth -> do
-                    Booster.Log.withContext "proxy" $
+                    Booster.Log.withContext CtxProxy $
                         Booster.Log.logMessage $
                             Text.pack $
                                 "Forced simplification at " <> show (currentDepth + boosterResult.depth)
@@ -336,7 +336,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                     case simplifyResult of
                         Left logsOnly -> do
                             -- state was simplified to \bottom, return vacuous
-                            Booster.Log.withContext "proxy" $
+                            Booster.Log.withContext CtxProxy $
                                 Booster.Log.logMessage $
                                     Text.pack "Vacuous state after simplification"
                             pure . Right . Execute $
@@ -365,12 +365,12 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                 -- if we stop for a reason in fallbackReasons (default [Aborted, Stuck, Branching],
                 -- revert to the old backend to re-confirm and possibly proceed
                 | boosterResult.reason `elem` cfg.fallbackReasons -> do
-                    Booster.Log.withContext "proxy" $
+                    Booster.Log.withContext CtxProxy $
                         Booster.Log.logMessage $
                             Text.pack $
                                 "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth
                     -- simplify Booster's state with Kore's simplifier
-                    Booster.Log.withContext "proxy" $
+                    Booster.Log.withContext CtxProxy $
                         Booster.Log.logMessage ("Simplifying booster state and falling back to Kore" :: Text)
                     simplifyResult <-
                         if cfg.simplifyBeforeFallback
@@ -379,13 +379,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                     case simplifyResult of
                         Left logsOnly -> do
                             -- state was simplified to \bottom, return vacuous
-                            Booster.Log.withContext "proxy" $
+                            Booster.Log.withContext CtxProxy $
                                 Booster.Log.logMessage $
                                     Text.pack "Vacuous state after simplification"
                             pure . Right . Execute $ makeVacuous (postProcessLogs <$> logsOnly) boosterResult
                         Right (simplifiedBoosterState, boosterStateSimplificationLogs) -> do
                             -- attempt to do one step in the old backend
-                            Booster.Log.withContext "proxy" $
+                            Booster.Log.withContext CtxProxy $
                                 Booster.Log.logMessage ("Executing fall-back request" :: Text)
                             (kResult, kTime) <-
                                 Stats.timed $
@@ -398,7 +398,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                                 }
                                         )
                             when (isJust statsVar) $ do
-                                Booster.Log.withContext "proxy" $
+                                Booster.Log.withContext CtxProxy $
                                     Booster.Log.logMessage $
                                         Text.pack $
                                             "Kore fall-back in " <> microsWithUnit kTime
@@ -432,19 +432,19 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                                 r{ExecuteRequest.state = nextState}
                                     case (boosterResult.reason, koreResult.reason) of
                                         (Aborted, res) ->
-                                            Booster.Log.withContext "proxy" $
-                                                Booster.Log.withContext "abort" $
+                                            Booster.Log.withContext CtxProxy $
+                                                Booster.Log.withContext CtxAbort $
                                                     Booster.Log.logMessage $
                                                         "Booster aborted, kore yields " <> Text.pack (show res)
                                         (bRes, kRes)
                                             | bRes /= kRes ->
-                                                Booster.Log.withContext "proxy" $
-                                                    Booster.Log.withContext "abort" $
+                                                Booster.Log.withContext CtxProxy $
+                                                    Booster.Log.withContext CtxAbort $
                                                         Booster.Log.logMessage $
                                                             "Booster and kore disagree: " <> Text.pack (show (bRes, kRes))
                                             | otherwise ->
-                                                Booster.Log.withContext "proxy" $
-                                                    Booster.Log.withContext "abort" $
+                                                Booster.Log.withContext CtxProxy $
+                                                    Booster.Log.withContext CtxAbort $
                                                         Booster.Log.logMessage $
                                                             "kore confirms result " <> Text.pack (show bRes)
 
@@ -454,7 +454,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                             -- steps we have taken to the counter and
                                             -- attempt with booster again
                                             when (koreResult.depth == 0) $ error "Expected kore-rpc to take at least one step"
-                                            Booster.Log.withContext "proxy" $
+                                            Booster.Log.withContext CtxProxy $
                                                 Booster.Log.logMessage $
                                                     Text.pack $
                                                         "kore depth-bound, continuing... (currently at "
@@ -465,7 +465,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                             -- otherwise we have hit a different
                                             -- HaltReason, at which point we should
                                             -- return, setting the correct depth
-                                            Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $
+                                            Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $
                                                 "Kore " <> show koreResult.reason <> " at " <> show koreResult.depth
                                             -- perform post-exec simplification.
                                             -- NB This has been found to make a difference,
@@ -499,7 +499,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                     -- we were successful with the booster, thus we
                     -- return the booster result with the updated
                     -- depth, in case we previously looped
-                    Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $
+                    Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $
                         "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth
                     -- perform post-exec simplification
                     postExecResult <-
@@ -543,7 +543,8 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
         mbModule
         def
         s = do
-            Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $ "Simplifying execution state"
+            Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $
+                "Simplifying execution state"
             simplResult <-
                 handleSimplify (toSimplifyRequest s) Nothing
             case simplResult of
@@ -576,13 +577,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                         , simplified.logs
                                         )
                             Left err -> do
-                                Booster.Log.withContext "proxy" . Booster.Log.logMessage $
+                                Booster.Log.withContext CtxProxy . Booster.Log.logMessage $
                                     "Error processing execute state simplification result: "
                                         <> Text.pack (show err)
                                 pure $ Right (s, Nothing)
                 _other -> do
                     -- if we hit an error here, return the original
-                    Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $
+                    Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $
                         "Unexpected failure when calling Kore simplifier, returning original term"
                     pure $ Right (s, Nothing)
           where
@@ -606,13 +607,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
     simplifyExecResult logSettings mbModule def res@ExecuteResult{reason, state, nextStates}
         | not cfg.simplifyAtEnd = pure $ Right res
         | otherwise = do
-            Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $
+            Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $
                 "Simplifying state in " <> show reason <> " result"
             simplified <- simplifyExecuteState logSettings mbModule def state
             case simplified of
                 Left logsOnly -> do
                     -- state simplified to \bottom, return vacuous
-                    Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $
+                    Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $
                         "Vacuous after simplifying result state"
                     pure . Right $ makeVacuous logsOnly res
                 Right (simplifiedState, simplifiedStateLogs) -> do
diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs
index f61487cf4d..a25e690179 100644
--- a/booster/tools/booster/Server.hs
+++ b/booster/tools/booster/Server.hs
@@ -57,7 +57,7 @@ import Booster.Definition.Ceil (ComputeCeilSummary (..), computeCeilsDefinition)
 import Booster.GlobalState
 import Booster.JsonRpc qualified as Booster
 import Booster.LLVM.Internal (mkAPI, withDLib)
-import Booster.Log qualified
+import Booster.Log hiding (withLogger)
 import Booster.Log.Context qualified
 import Booster.Pattern.Base (Predicate (..))
 import Booster.Prettyprinter (renderOneLineText)
@@ -193,7 +193,7 @@ main = do
             filteredBoosterContextLogger =
                 flip Booster.Log.filterLogger boosterContextLogger $ \(Booster.Log.LogMessage (Booster.Flag alwaysDisplay) ctxts _) ->
                     alwaysDisplay
-                        || let ctxt = map (\(Booster.Log.LogContext lc) -> Text.encodeUtf8 $ Booster.Log.toTextualLog lc) ctxts
+                        || let ctxt = map (Text.encodeUtf8 . Booster.Log.toTextualLog) ctxts
                             in any (flip Booster.Log.Context.mustMatch ctxt) logContextsWithcustomLevelContexts
 
             runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a
@@ -209,7 +209,7 @@ main = do
                         (fromMaybe stderrLogger mFileLogger)
 
         runBoosterLogger $
-            Booster.Log.withContext "proxy" $
+            Booster.Log.withContext CtxProxy $
                 Booster.Log.logMessage' $
                     Text.pack $
                         "Loading definition from "
@@ -239,18 +239,18 @@ main = do
                             >>= evaluate . force . either (error . show) id
                 unless (isJust $ Map.lookup mainModuleName definitionsWithCeilSummaries) $ do
                     runBoosterLogger $
-                        Booster.Log.withContext "proxy" $
+                        Booster.Log.withContext CtxProxy $
                             Booster.Log.logMessage' $
                                 "Main module " <> mainModuleName <> " not found in " <> Text.pack definitionFile
                     liftIO exitFailure
 
                 liftIO $
                     runBoosterLogger $
-                        Booster.Log.withContext "ceil" $
+                        Booster.Log.withContext CtxInfo $ -- FIXME "ceil" $
                             forM_ (Map.elems definitionsWithCeilSummaries) $ \(KoreDefinition{simplifications}, summaries) -> do
                                 forM_ summaries $ \ComputeCeilSummary{rule, ceils} ->
                                     Booster.Log.withRuleContext rule $ do
-                                        Booster.Log.withContext "partial-symbols"
+                                        Booster.Log.withContext CtxInfo -- FIXME "partial-symbols"
                                             $ Booster.Log.logMessage
                                             $ Booster.Log.WithJsonMessage
                                                 (JSON.toJSON rule.computedAttributes.notPreservesDefinednessReasons)
@@ -261,7 +261,7 @@ main = do
                                                 (\(UndefinedSymbol sym) -> Pretty.pretty $ Text.decodeUtf8 $ Booster.decodeLabel' sym)
                                                 rule.computedAttributes.notPreservesDefinednessReasons
                                         unless (null ceils)
-                                            $ Booster.Log.withContext "computed-ceils"
+                                            $ Booster.Log.withContext CtxInfo -- FIXME"computed-ceils"
                                             $ Booster.Log.logMessage
                                             $ Booster.Log.WithJsonMessage
                                                 ( JSON.object
@@ -277,7 +277,7 @@ main = do
                                 forM_ (concat $ concatMap Map.elems simplifications) $ \s ->
                                     unless (null s.computedAttributes.notPreservesDefinednessReasons)
                                         $ Booster.Log.withRuleContext s
-                                        $ Booster.Log.withContext "partial-symbols"
+                                        $ Booster.Log.withContext CtxInfo -- FIXME"partial-symbols"
                                         $ Booster.Log.logMessage
                                         $ Booster.Log.WithJsonMessage
                                             (JSON.toJSON s.computedAttributes.notPreservesDefinednessReasons)
@@ -308,13 +308,13 @@ main = do
                 writeGlobalEquationOptions equationOptions
 
                 runBoosterLogger $
-                    Booster.Log.withContext "proxy" $
+                    Booster.Log.withContext CtxProxy $
                         Booster.Log.logMessage' ("Starting RPC server" :: Text)
 
                 let koreRespond, boosterRespond :: Respond (API 'Req) (Booster.Log.LoggerT IO) (API 'Res)
                     koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT
                     boosterRespond =
-                        Booster.Log.withContext "booster"
+                        Booster.Log.withContext CtxBooster
                             . Booster.respond boosterState
 
                     proxyConfig =
@@ -341,7 +341,7 @@ main = do
                             , handleSomeException
                             ]
                     interruptHandler _ =
-                        runBoosterLogger . Booster.Log.withContext "proxy" $ do
+                        runBoosterLogger . Booster.Log.withContext CtxProxy $ do
                             Booster.Log.logMessage' @_ @Text "Server shutting down"
                             whenJust statsVar $ \var ->
                                 liftIO (Stats.finaliseStats var) >>= Booster.Log.logMessage'
@@ -357,7 +357,7 @@ main = do
     withMDLib (Just fp) f = withDLib fp $ \dl -> f (Just dl)
 
     logRequestId rid =
-        Booster.Log.withContext "proxy" $
+        Booster.Log.withContext CtxProxy $
             Booster.Log.logMessage' $
                 Text.pack $
                     "Processing request " <> rid
diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs
index 638d0a76e2..abb3855b7c 100644
--- a/dev-tools/booster-dev/Server.hs
+++ b/dev-tools/booster-dev/Server.hs
@@ -143,7 +143,7 @@ runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLev
                 filteredBoosterContextLogger =
                     flip Booster.Log.filterLogger boosterContextLogger $ \(Booster.Log.LogMessage (Booster.Flag alwaysDisplay) ctxts _) ->
                         alwaysDisplay
-                            || let ctxt = map (\(Booster.Log.LogContext lc) -> Text.encodeUtf8 $ Booster.Log.toTextualLog lc) ctxts
+                            || let ctxt = map (Text.encodeUtf8 . Booster.Log.toTextualLog) ctxts
                                 in any (flip Booster.Log.mustMatch ctxt) $
                                     logContexts
                                         <> concatMap (\case Log.LevelOther o -> fromMaybe [] $ levelToContext Map.!? o; _ -> []) customLevels
@@ -161,7 +161,7 @@ runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLev
                 ( const $
                     flip runReaderT filteredBoosterContextLogger
                         . Booster.Log.unLoggerT
-                        . Booster.Log.withContext "booster"
+                        . Booster.Log.withContext Booster.Log.CtxBooster
                         . respond stateVar
                 )
                 [handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException]
diff --git a/dev-tools/count-aborts/Main.hs b/dev-tools/count-aborts/Main.hs
index 4b955a3fe9..411f6804a1 100644
--- a/dev-tools/count-aborts/Main.hs
+++ b/dev-tools/count-aborts/Main.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE PatternSynonyms #-}
+
 {- | Stand-alone parser executable for testing and profiling
 
 Copyright   : (c) Runtime Verification, 2022
@@ -11,13 +13,17 @@ import Control.Monad (foldM, forM_)
 import Data.Aeson (decode)
 import Data.ByteString.Lazy.Char8 qualified as BS
 import Data.List (foldl', sortOn)
+import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Ord (Down (..))
+import Data.Sequence (Seq (..))
+import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Text.IO qualified as T
 import System.Environment (getArgs)
-import Types
+
+import Kore.JsonRpc.Types.ContextLog
 
 {- | Utility for parsing and extracting information from context logs,
    produced by running the booster binary with `--log-format json --log-file <path>`.
@@ -40,4 +46,31 @@ main =
                 forM_ (sortOn (Down . snd) $ Map.toList counts) $ \((rule, reason), count) -> do
                     let (rType, rLoc) = fromMaybe ("-", "-") $ Map.lookup rule rIdTorLoc
                     T.putStrLn . T.unwords $
-                        map ("| " <>) [rType <> " " <> rule, rLoc, reason, T.pack (show count)]
+                        map ("| " <>) [rType <> " " <> T.pack (show rule), rLoc, T.pack (show reason), T.pack (show count)]
+
+type AbortKey = (UniqueId, SimpleContext)
+
+pattern CRewrite, CFunction, CSimpl :: UniqueId -> CLContext
+pattern CRewrite r = CLWithId (CtxRewrite r)
+pattern CFunction r = CLWithId (CtxFunction r)
+pattern CSimpl r = CLWithId (CtxSimplification r)
+
+pattern C :: SimpleContext -> CLContext
+pattern C ctx = CLNullary ctx
+
+countAborts ::
+    (Map AbortKey Int, Map UniqueId (Text, Text)) ->
+    LogLine ->
+    (Map AbortKey Int, Map UniqueId (Text, Text))
+countAborts maps@(countMap, ruleMap) LogLine{context, message} = case context of
+    (_ :|> CRewrite ruleId :|> C reason :|> C CtxAbort) -> increment reason ruleId
+    (_ :|> CFunction ruleId :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId
+    (_ :|> CSimpl ruleId :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId
+    (_ :|> CFunction ruleId :|> C CtxMatch :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId
+    (_ :|> CSimpl ruleId :|> C CtxMatch :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId
+    (_ :|> CRewrite ruleId :|> C CtxDetail) | CLText ruleLoc <- message -> (countMap, Map.insert ruleId ("rewrite", ruleLoc) ruleMap)
+    (_ :|> CFunction ruleId :|> C CtxDetail) | CLText ruleLoc <- message -> (countMap, Map.insert ruleId ("function", ruleLoc) ruleMap)
+    (_ :|> CSimpl ruleId :|> C CtxDetail) | CLText ruleLoc <- message -> (countMap, Map.insert ruleId ("simplification", ruleLoc) ruleMap)
+    _ -> maps
+  where
+    increment rsn rid = (Map.alter (maybe (Just 1) (Just . (+ 1))) (rid, rsn) countMap, ruleMap)
diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs
index f6914b620b..6e4ca8b5d5 100644
--- a/dev-tools/kore-rpc-dev/Server.hs
+++ b/dev-tools/kore-rpc-dev/Server.hs
@@ -97,7 +97,7 @@ respond kore req = case req of
     Execute _ ->
         loggedKore ExecuteM req >>= \case
             Right (Execute koreResult) -> do
-                withContext "proxy" $
+                withContext CtxKore $
                     logMessage $
                         Text.pack $
                             "Kore " <> show koreResult.reason <> " at " <> show koreResult.depth
@@ -126,7 +126,7 @@ respond kore req = case req of
                 pure koreError
 
     loggedKore method r = do
-        withContext "proxy" $
+        withContext CtxKore $
             logMessage' $
                 Text.pack $
                     show method <> " (using kore)"
@@ -217,7 +217,7 @@ main = do
             filteredBoosterContextLogger =
                 flip filterLogger boosterContextLogger $ \(LogMessage (Booster.Flag alwaysDisplay) ctxts _) ->
                     alwaysDisplay
-                        || let ctxt = map (\(LogContext lc) -> Text.encodeUtf8 $ toTextualLog lc) ctxts
+                        || let ctxt = map (Text.encodeUtf8 . toTextualLog) ctxts
                             in any (flip Booster.Log.Context.mustMatch ctxt) logContextsWithcustomLevelContexts
 
             runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a
@@ -230,7 +230,7 @@ main = do
                 kore@KoreServer{runSMT} <-
                     mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions
                 runBoosterLogger $
-                    Booster.Log.withContext "proxy" $
+                    Booster.Log.withContext CtxKore $
                         Booster.Log.logMessage' ("Starting RPC server" :: Text.Text)
 
                 let koreRespond :: Respond (API 'Req) (LoggerT IO) (API 'Res)
diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml
index aea7fcccc1..749a928d8b 100644
--- a/dev-tools/package.yaml
+++ b/dev-tools/package.yaml
@@ -99,6 +99,7 @@ executables:
       - containers
       - directory
       - filepath
+      - kore-rpc-types
       - text
     ghc-options:
       - -rtsopts
diff --git a/kore-rpc-types/kore-rpc-types.cabal b/kore-rpc-types/kore-rpc-types.cabal
index 107f12e1bc..61519e6237 100644
--- a/kore-rpc-types/kore-rpc-types.cabal
+++ b/kore-rpc-types/kore-rpc-types.cabal
@@ -67,6 +67,7 @@ common library
   build-depends: casing >= 0.1.4
   build-depends: conduit >= 1.3
   build-depends: conduit-extra >=1.3
+  build-depends: containers >= 0.6
   build-depends: deepseq >=1.4
   build-depends: extra >=1.7
   build-depends: deriving-aeson >=0.2
@@ -77,6 +78,7 @@ common library
   build-depends: stm >=2.5
   build-depends: stm-conduit >= 4.0
   build-depends: text >=1.2
+  build-depends: time
   build-depends: unliftio >= 0.2
   build-depends: vector >= 0.12.3.1
 
@@ -88,6 +90,7 @@ library
     Kore.JsonRpc.Error
     Kore.JsonRpc.Types
     Kore.JsonRpc.Types.Log
+    Kore.JsonRpc.Types.ContextLog
     Kore.JsonRpc.Types.Depth
     Kore.JsonRpc.Server
     Kore.Syntax.Json.Types
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
new file mode 100644
index 0000000000..dc87190377
--- /dev/null
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -0,0 +1,178 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2023
+License     : BSD-3-Clause
+-}
+module Kore.JsonRpc.Types.ContextLog (
+    module Kore.JsonRpc.Types.ContextLog,
+) where
+
+import Data.Aeson.TH (deriveJSON)
+import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions)
+import Data.Aeson.Types qualified as JSON
+import Data.Data (Data, toConstr)
+import Data.Sequence (Seq)
+import Data.Text (Text, unpack)
+import Data.Text qualified as Text
+
+data SimpleContext
+    = -- component
+      CtxBooster
+    | CtxKore
+    | CtxProxy
+    | -- method
+      CtxExecute
+    | CtxSimplify
+    | CtxImplies
+    | CtxGetModel
+    | CtxAddModule
+    | -- mode/phase
+      CtxInternalise
+    | CtxMatch
+    | CtxDefinedness
+    | CtxConstraint
+    | CtxSMT
+    | CtxLlvm
+    | CtxCached
+    | -- results
+      CtxFailure
+    | CtxIndeterminate
+    | CtxAbort
+    | CtxSuccess
+    | CtxBreak
+    | CtxContinue
+    | -- information
+      CtxKoreTerm
+    | CtxDetail
+    | CtxSubstitution
+    | CtxDepth
+    | -- standard log levels
+      CtxError
+    | CtxWarn
+    | CtxInfo
+    deriving stock (Eq, Ord, Enum, Data)
+
+instance Show SimpleContext where
+    show = JSON.camelTo2 '-' . drop 3 . show . toConstr
+
+$( deriveJSON
+    defaultOptions
+        { JSON.constructorTagModifier = JSON.camelTo2 '-' . drop 3
+        , JSON.sumEncoding = JSON.ObjectWithSingleField
+        }
+    ''SimpleContext
+ )
+
+----------------------------------------
+data IdContext
+    = -- entities with hex identifier
+      CtxRewrite UniqueId
+    | CtxSimplification UniqueId
+    | CtxFunction UniqueId
+    | CtxCeil UniqueId
+    | CtxTerm UniqueId
+    | -- entities with name
+      CtxHook Text
+    deriving stock (Eq)
+
+instance Show IdContext where
+    show (CtxRewrite uid) = "rewrite " <> show uid
+    show (CtxSimplification uid) = "simplification " <> show uid
+    show (CtxFunction uid) = "function " <> show uid
+    show (CtxCeil uid) = "ceil " <> show uid
+    show (CtxTerm uid) = "term " <> show uid
+    show (CtxHook name) = "hook " <> unpack name
+
+----------------------------------------
+data UniqueId
+    = ShortId Text -- short hashes (7 char)
+    | LongId Text -- long hashes (64 char)
+    | UNKNOWN
+    deriving stock (Eq, Ord)
+
+instance Show UniqueId where
+    show (ShortId x) = unpack x
+    show (LongId x) = unpack $ Text.take 7 x -- for parity with legacy log
+    show UNKNOWN = "UNKNOWN"
+
+parseUId :: Text -> Maybe UniqueId
+parseUId "UNKNOWN" = pure UNKNOWN
+parseUId hex
+    | Text.length hex == 7 = Just $ ShortId hex
+    | Text.length hex == 64 = Just $ LongId hex
+    | otherwise = Nothing
+
+instance FromJSON UniqueId where
+    parseJSON = JSON.withText "Hash ID" parseHex
+      where
+        parseHex :: Text -> JSON.Parser UniqueId
+        parseHex hex =
+            maybe (JSON.parseFail $ "Bad hash ID: " <> show hex) pure $ parseUId hex
+
+instance ToJSON UniqueId where
+    toJSON = \case
+        ShortId x -> JSON.String x
+        LongId x -> JSON.String x
+        UNKNOWN -> JSON.String "UNKNOWN"
+
+$( deriveJSON
+    defaultOptions
+        { JSON.constructorTagModifier = JSON.camelTo2 '-' . drop 3
+        , JSON.sumEncoding = JSON.ObjectWithSingleField
+        }
+    ''IdContext
+ )
+
+----------------------------------------
+data CLContext
+    = CLNullary SimpleContext
+    | CLWithId IdContext
+    deriving stock (Eq)
+
+instance Show CLContext where
+    show (CLNullary c) = show c
+    show (CLWithId withId) = show withId
+
+instance ToJSON CLContext where
+    toJSON (CLNullary c) = toJSON c
+    toJSON (CLWithId withId) = toJSON withId
+
+instance FromJSON CLContext where
+    parseJSON = \case
+        simple@JSON.String{} ->
+            CLNullary <$> parseJSON simple
+        obj@JSON.Object{} ->
+            CLWithId <$> parseJSON obj
+        other ->
+            JSON.typeMismatch "Object or string" other
+
+----------------------------------------
+data CLMessage
+    = CLText Text -- generic log message
+    | CLValue JSON.Value -- other stuff
+    deriving stock (Eq)
+
+instance Show CLMessage where
+    show (CLText t) = unpack t
+    show (CLValue value) = show value
+
+-- a message is a term if it is an object with format: KORE
+instance FromJSON CLMessage where
+    parseJSON (JSON.String msg) = pure $ CLText msg
+    parseJSON obj@JSON.Object{} = pure $ CLValue obj
+    parseJSON arr@JSON.Array{} = pure $ CLValue arr
+    parseJSON other =
+        JSON.typeMismatch "Object, array, or string" other
+
+instance ToJSON CLMessage where
+    toJSON (CLText text) = toJSON text
+    toJSON (CLValue value) = value
+
+data LogLine = LogLine
+    { context :: Seq CLContext
+    , message :: CLMessage
+    }
+    deriving stock (Show, Eq)
+
+$(deriveJSON defaultOptions ''LogLine)