From 2362d3e4c90875e211a4f2f1164eedc28c70ef9f Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Fri, 31 May 2024 19:42:10 +1000
Subject: [PATCH 01/16] Prior art: beginnings of parsing json context log

---
 kore-rpc-types/kore-rpc-types.cabal           |   2 +
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 189 ++++++++++++++++++
 2 files changed, 191 insertions(+)
 create mode 100644 kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs

diff --git a/kore-rpc-types/kore-rpc-types.cabal b/kore-rpc-types/kore-rpc-types.cabal
index 107f12e1bc..0c7e74eb26 100644
--- a/kore-rpc-types/kore-rpc-types.cabal
+++ b/kore-rpc-types/kore-rpc-types.cabal
@@ -77,6 +77,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 +89,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..3d9a30ac77
--- /dev/null
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -0,0 +1,189 @@
+{-# OPTIONS_GHC -Wno-partial-fields #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2023
+License     : BSD-3-Clause
+-}
+module Kore.JsonRpc.Types.ContextLog (
+    module Kore.JsonRpc.Types.ContextLog,
+) where
+
+import Control.Applicative ((<|>))
+import Data.Aeson.Types (FromJSON (..), ToJSON (..), (.:))
+import Data.Aeson.Types qualified as JSON
+import Data.Aeson.KeyMap qualified as JSON
+import Data.List (stripPrefix)
+import Data.Maybe (fromMaybe)
+import Data.Text (Text, pack, unpack)
+import Data.Time
+import Deriving.Aeson
+import Numeric
+
+import Kore.Syntax.Json.Types (KoreJson, KORE)
+
+-- | result type
+data ContextLog
+    = CtxLog
+      { context :: [CLContext]
+      , entries :: [ContextLog]
+      , timestamp :: Maybe TimeOfDay
+      , duration :: Maybe DiffTime
+      }
+    | CLEntry
+      { message :: Maybe Text
+      , term :: Maybe KoreJson
+      }
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[OmitNothingFields] ContextLog
+
+data CLContext
+    = CtxBooster
+    | CtxKore
+    -- "modes"
+    | CtxExecute
+    | CtxSimplify
+    | CtxImplies
+    | CtxGetModel
+    | CtxMatch
+    -- entities with hex identifier
+    | CtxRewrite UniqueId
+    | CtxSimplification UniqueId
+    | CtxFunction UniqueId
+    | CtxTerm UniqueId
+    -- entities with name
+    | CtxHook Text
+    -- results
+    | CtxFailure
+    | CtxAbort
+    | CtxSuccess
+    -- information
+    | CtxKoreTerm
+    | CtxDetail
+    -- standard log levels
+    | CtxError
+    | CtxWarn
+    | CtxInfo
+    -- free-form
+    | Ctx Text
+    deriving stock (Generic, Show, Eq)
+
+instance ToJSON CLContext where
+    -- nullary constructors encoded as simple strings
+    toJSON = \case
+        CtxBooster -> JSON.String $ camelToKebab "Booster"
+        CtxKore -> JSON.String $ camelToKebab "Kore"
+        CtxExecute -> JSON.String $ camelToKebab "Execute"
+        CtxSimplify -> JSON.String $ camelToKebab "Simplify"
+        CtxImplies -> JSON.String $ camelToKebab "Implies"
+        CtxGetModel -> JSON.String $ camelToKebab "GetModel"
+        CtxMatch -> JSON.String $ camelToKebab "Match"
+        CtxFailure -> JSON.String $ camelToKebab "Failure"
+        CtxAbort -> JSON.String $ camelToKebab "Abort"
+        CtxSuccess -> JSON.String $ camelToKebab "Success"
+        CtxKoreTerm -> JSON.String $ camelToKebab "KoreTerm"
+        CtxDetail -> JSON.String $ camelToKebab "Detail"
+        CtxError -> JSON.String $ camelToKebab "Error"
+        CtxWarn -> JSON.String $ camelToKebab "Warn"
+        CtxInfo -> JSON.String $ camelToKebab "Info"
+        Ctx txt-> JSON.String txt
+        -- entities with hex identifier
+        other -> JSON.genericToJSON options other
+
+instance FromJSON CLContext where
+    parseJSON = \case
+        JSON.String "booster" -> pure CtxBooster
+        JSON.String "kore" -> pure CtxKore
+        JSON.String "execute" -> pure CtxExecute
+        JSON.String "simplify" -> pure CtxSimplify
+        JSON.String "implies" -> pure CtxImplies
+        JSON.String "get-model" -> pure CtxGetModel
+        JSON.String "match" -> pure CtxMatch
+        JSON.String "failure" -> pure CtxFailure
+        JSON.String "abort" -> pure CtxAbort
+        JSON.String "success" -> pure CtxSuccess
+        JSON.String "kore-term" -> pure CtxKoreTerm
+        JSON.String "detail" -> pure CtxDetail
+        JSON.String "error" -> pure CtxError
+        JSON.String "warn" -> pure CtxWarn
+        JSON.String "info" -> pure CtxInfo
+        JSON.String other -> pure $ Ctx other
+
+        obj -> JSON.genericParseJSON options obj
+
+camelToKebab :: String -> Text
+camelToKebab = pack . JSON.camelTo2 '-'
+
+options :: JSON.Options
+options =
+    JSON.defaultOptions
+    { JSON.sumEncoding = JSON.ObjectWithSingleField
+    , JSON.constructorTagModifier = \name ->
+            JSON.camelTo2 '-' $ fromMaybe name $ stripPrefix "Ctx" name
+    , JSON.allNullaryToStringTag = True
+    }
+
+data LogLine
+    = LogLine
+      { context :: [CLContext]
+      , message :: CLMessage
+      }
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[] LogLine
+
+data CLMessage
+    = CLText Text  -- generic log message
+    | CLArray [Text] -- array of partial symbol names (ceil analysis)
+    | CLTerm KoreJson -- kore-term
+    | CLId JSON.Key UniqueId -- simplification/rewrite/match success
+    deriving stock (Generic, Show, Eq)
+
+-- a message is a term if it is an object with format: KORE
+instance FromJSON CLMessage where
+    parseJSON obj@(JSON.Object o) =
+        parseTerm <|> parseId
+      where
+        parseTerm = do
+            _ :: KORE <- o .: "format" -- must be KORE
+            CLTerm <$> parseJSON obj
+        parseId = case JSON.toList o of
+            [(aKey, uniqueId)] -> CLId aKey <$> parseJSON uniqueId
+            _other -> JSON.typeMismatch "Singleton object" obj
+    parseJSON (JSON.String msg) =
+        pure $ CLText msg
+    parseJSON arr@JSON.Array{} =
+        CLArray <$> parseJSON arr
+    parseJSON other =
+        JSON.typeMismatch "Object, array, or string" other
+
+instance ToJSON CLMessage where
+    toJSON (CLText text) = toJSON text
+    toJSON (CLArray msgs) = toJSON msgs
+    toJSON (CLTerm term) = toJSON term
+    toJSON (CLId key uniqueId) = JSON.Object $ JSON.singleton key (toJSON uniqueId)
+
+data UniqueId
+    = Hex Integer
+    | UNKNOWN
+    deriving stock (Generic, Eq, Ord)
+
+instance Show UniqueId where
+    show (Hex i) = showHex i ""
+    show UNKNOWN = "UNKNOWN"
+
+instance FromJSON UniqueId where
+    parseJSON = JSON.withText "Hexadecimal Hash" parseHex
+      where
+        parseHex :: Text -> JSON.Parser UniqueId
+        parseHex "UNKNOWN" = pure UNKNOWN
+        parseHex hex =
+            case readHex $ unpack hex of
+                [(h, "")] -> pure  $ Hex h
+                _otherwise -> JSON.parseFail $ "Bad hash value: " <> show hex
+
+instance ToJSON UniqueId where
+    toJSON (Hex x) = JSON.String . pack $ showHex x ""
+    toJSON UNKNOWN = JSON.String "UNKNOWN"

From 31e682bb541d4b07025b3c35b0b20a6a0d23a903 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 18 Jun 2024 15:25:37 +1000
Subject: [PATCH 02/16] adjust context type, reduce logline type just for
 testing

---
 kore-rpc-types/kore-rpc-types.cabal           |   1 +
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 254 +++++++++---------
 2 files changed, 126 insertions(+), 129 deletions(-)

diff --git a/kore-rpc-types/kore-rpc-types.cabal b/kore-rpc-types/kore-rpc-types.cabal
index 0c7e74eb26..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
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 3d9a30ac77..0b43643400 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -8,52 +8,68 @@ module Kore.JsonRpc.Types.ContextLog (
     module Kore.JsonRpc.Types.ContextLog,
 ) where
 
-import Control.Applicative ((<|>))
-import Data.Aeson.Types (FromJSON (..), ToJSON (..), (.:))
+import Data.Aeson.Types (FromJSON (..), ToJSON (..))
 import Data.Aeson.Types qualified as JSON
-import Data.Aeson.KeyMap qualified as JSON
+import Data.Data
 import Data.List (stripPrefix)
+import Data.Map (Map)
+import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Text (Text, pack, unpack)
-import Data.Time
+import Data.Text qualified as Text
+import Data.Tuple (swap)
 import Deriving.Aeson
 import Numeric
 
-import Kore.Syntax.Json.Types (KoreJson, KORE)
+data CLContext
+    = CLNullary SimpleContext
+    | CLWithId IdContext
+    deriving stock (Generic, Eq)
 
--- | result type
-data ContextLog
-    = CtxLog
-      { context :: [CLContext]
-      , entries :: [ContextLog]
-      , timestamp :: Maybe TimeOfDay
-      , duration :: Maybe DiffTime
-      }
-    | CLEntry
-      { message :: Maybe Text
-      , term :: Maybe KoreJson
-      }
-    deriving stock (Generic, Show, Eq)
-    deriving
-        (FromJSON, ToJSON)
-        via CustomJSON '[OmitNothingFields] ContextLog
+instance Show CLContext where
+    show (CLNullary c) = fromMaybe (error $ show c) $ Map.lookup c simpleShow
+    show (CLWithId withId) = show withId
 
-data CLContext
-    = CtxBooster
+instance ToJSON CLContext where
+    toJSON (CLNullary c) = JSON.String $ maybe (error $ show c) pack $ Map.lookup c simpleShow
+    toJSON (CLWithId withId) = JSON.genericToJSON options withId
+
+instance FromJSON CLContext where
+    parseJSON = \case
+        JSON.String simple
+            | Just c <- Map.lookup (unpack simple) simpleRead ->
+                pure $ CLNullary c
+        obj@JSON.Object{} ->
+            CLWithId <$> JSON.genericParseJSON options obj
+        other ->
+            JSON.typeMismatch "Object or string" other
+
+options :: JSON.Options
+options =
+    JSON.defaultOptions
+    { JSON.sumEncoding = JSON.ObjectWithSingleField
+    , JSON.constructorTagModifier = toJsonName
+    , JSON.allNullaryToStringTag = True
+    }
+
+toJsonName :: String -> String
+toJsonName name = JSON.camelTo2 '-' $ fromMaybe name $ stripPrefix "Ctx" name
+
+----------------------------------------
+data SimpleContext
+    = -- component
+      CtxBooster
     | CtxKore
-    -- "modes"
+    | CtxProxy
+    -- method
     | CtxExecute
     | CtxSimplify
     | CtxImplies
     | CtxGetModel
+    -- mode/phase
     | CtxMatch
-    -- entities with hex identifier
-    | CtxRewrite UniqueId
-    | CtxSimplification UniqueId
-    | CtxFunction UniqueId
-    | CtxTerm UniqueId
-    -- entities with name
-    | CtxHook Text
+    | CtxDefinedness
+    | CtxConstraint
     -- results
     | CtxFailure
     | CtxAbort
@@ -65,113 +81,51 @@ data CLContext
     | CtxError
     | CtxWarn
     | CtxInfo
-    -- free-form
-    | Ctx Text
-    deriving stock (Generic, Show, Eq)
+    deriving stock (Generic, Data, Enum, Show, Eq, Ord)
 
-instance ToJSON CLContext where
-    -- nullary constructors encoded as simple strings
-    toJSON = \case
-        CtxBooster -> JSON.String $ camelToKebab "Booster"
-        CtxKore -> JSON.String $ camelToKebab "Kore"
-        CtxExecute -> JSON.String $ camelToKebab "Execute"
-        CtxSimplify -> JSON.String $ camelToKebab "Simplify"
-        CtxImplies -> JSON.String $ camelToKebab "Implies"
-        CtxGetModel -> JSON.String $ camelToKebab "GetModel"
-        CtxMatch -> JSON.String $ camelToKebab "Match"
-        CtxFailure -> JSON.String $ camelToKebab "Failure"
-        CtxAbort -> JSON.String $ camelToKebab "Abort"
-        CtxSuccess -> JSON.String $ camelToKebab "Success"
-        CtxKoreTerm -> JSON.String $ camelToKebab "KoreTerm"
-        CtxDetail -> JSON.String $ camelToKebab "Detail"
-        CtxError -> JSON.String $ camelToKebab "Error"
-        CtxWarn -> JSON.String $ camelToKebab "Warn"
-        CtxInfo -> JSON.String $ camelToKebab "Info"
-        Ctx txt-> JSON.String txt
-        -- entities with hex identifier
-        other -> JSON.genericToJSON options other
+-- translation table for nullary constructors
+translateSimple :: [(SimpleContext, String)]
+translateSimple =
+    [ (con, toJsonName $ show con)
+    | con <- [CtxBooster .. CtxInfo]
+    ]
 
-instance FromJSON CLContext where
-    parseJSON = \case
-        JSON.String "booster" -> pure CtxBooster
-        JSON.String "kore" -> pure CtxKore
-        JSON.String "execute" -> pure CtxExecute
-        JSON.String "simplify" -> pure CtxSimplify
-        JSON.String "implies" -> pure CtxImplies
-        JSON.String "get-model" -> pure CtxGetModel
-        JSON.String "match" -> pure CtxMatch
-        JSON.String "failure" -> pure CtxFailure
-        JSON.String "abort" -> pure CtxAbort
-        JSON.String "success" -> pure CtxSuccess
-        JSON.String "kore-term" -> pure CtxKoreTerm
-        JSON.String "detail" -> pure CtxDetail
-        JSON.String "error" -> pure CtxError
-        JSON.String "warn" -> pure CtxWarn
-        JSON.String "info" -> pure CtxInfo
-        JSON.String other -> pure $ Ctx other
-
-        obj -> JSON.genericParseJSON options obj
-
-camelToKebab :: String -> Text
-camelToKebab = pack . JSON.camelTo2 '-'
+simpleShow :: Map SimpleContext String
+simpleShow = Map.fromList translateSimple
 
-options :: JSON.Options
-options =
-    JSON.defaultOptions
-    { JSON.sumEncoding = JSON.ObjectWithSingleField
-    , JSON.constructorTagModifier = \name ->
-            JSON.camelTo2 '-' $ fromMaybe name $ stripPrefix "Ctx" name
-    , JSON.allNullaryToStringTag = True
-    }
+simpleRead :: Map String SimpleContext
+simpleRead = Map.fromList $ map swap translateSimple
 
-data LogLine
-    = LogLine
-      { context :: [CLContext]
-      , message :: CLMessage
-      }
-    deriving stock (Generic, Show, Eq)
-    deriving
-        (FromJSON, ToJSON)
-        via CustomJSON '[] LogLine
-
-data CLMessage
-    = CLText Text  -- generic log message
-    | CLArray [Text] -- array of partial symbol names (ceil analysis)
-    | CLTerm KoreJson -- kore-term
-    | CLId JSON.Key UniqueId -- simplification/rewrite/match success
-    deriving stock (Generic, Show, Eq)
+----------------------------------------
+data IdContext
+    = -- entities with hex identifier
+      CtxRewrite UniqueId
+    | CtxSimplification UniqueId
+    | CtxFunction UniqueId
+    | CtxTerm UniqueId
+    -- entities with name
+    | CtxHook Text
+    deriving stock (Generic, Eq)
 
--- a message is a term if it is an object with format: KORE
-instance FromJSON CLMessage where
-    parseJSON obj@(JSON.Object o) =
-        parseTerm <|> parseId
-      where
-        parseTerm = do
-            _ :: KORE <- o .: "format" -- must be KORE
-            CLTerm <$> parseJSON obj
-        parseId = case JSON.toList o of
-            [(aKey, uniqueId)] -> CLId aKey <$> parseJSON uniqueId
-            _other -> JSON.typeMismatch "Singleton object" obj
-    parseJSON (JSON.String msg) =
-        pure $ CLText msg
-    parseJSON arr@JSON.Array{} =
-        CLArray <$> parseJSON arr
-    parseJSON other =
-        JSON.typeMismatch "Object, array, or string" other
+-- To/FromJSON by way of Generic
 
-instance ToJSON CLMessage where
-    toJSON (CLText text) = toJSON text
-    toJSON (CLArray msgs) = toJSON msgs
-    toJSON (CLTerm term) = toJSON term
-    toJSON (CLId key uniqueId) = JSON.Object $ JSON.singleton key (toJSON uniqueId)
+instance Show IdContext where
+    show (CtxRewrite uid) = "rewrite " <> show uid
+    show (CtxSimplification uid) = "simplification " <> show uid
+    show (CtxFunction uid) = "function " <> show uid
+    show (CtxTerm uid) = "term " <> show uid
+    show (CtxHook name) = "simplification " <> unpack name
 
+----------------------------------------
 data UniqueId
-    = Hex Integer
+    = Hex7 Integer -- short hashes (7 char)
+    | Hex64 Integer -- long hashes (64 char)
     | UNKNOWN
     deriving stock (Generic, Eq, Ord)
 
 instance Show UniqueId where
-    show (Hex i) = showHex i ""
+    show (Hex7 i) = showHex i ""
+    show (Hex64 i) = showHex i "" -- or show shortened version?
     show UNKNOWN = "UNKNOWN"
 
 instance FromJSON UniqueId where
@@ -181,9 +135,51 @@ instance FromJSON UniqueId where
         parseHex "UNKNOWN" = pure UNKNOWN
         parseHex hex =
             case readHex $ unpack hex of
-                [(h, "")] -> pure  $ Hex h
+                [(h, "")]
+                    | Text.length hex < 8 -> pure $ Hex7 h
+                    | Text.length hex <= 64 -> pure $ Hex64 h
                 _otherwise -> JSON.parseFail $ "Bad hash value: " <> show hex
 
 instance ToJSON UniqueId where
-    toJSON (Hex x) = JSON.String . pack $ showHex x ""
-    toJSON UNKNOWN = JSON.String "UNKNOWN"
+    toJSON = \case
+        Hex7 x ->
+            JSON.String . pad0 7 . pack $ showHex x ""
+        Hex64 x ->
+            JSON.String . pad0 64 . pack $ showHex x ""
+        UNKNOWN ->
+            JSON.String "UNKNOWN"
+      where
+          pad0 l = Text.takeEnd l . (Text.replicate l "0" <>)
+
+
+----------------------------------------
+data LogLine
+    = LogLine
+      { context :: [CLContext]
+      , message :: CLMessage
+      }
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[] LogLine
+
+data CLMessage
+    = CLText Text  -- generic log message
+    | CLValue JSON.Value -- other stuff
+    deriving stock (Generic, 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

From 70c8168ecebe2a038fa896a14d9df2c160c391ac Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 18 Jun 2024 16:48:21 +1000
Subject: [PATCH 03/16] WIP converting booster context logs to typed context

---
 booster/library/Booster/Log.hs                | 76 +++++++++----------
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 20 +++--
 2 files changed, 47 insertions(+), 49 deletions(-)

diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index b6b96d6d02..98add28cac 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}
@@ -23,13 +24,17 @@ 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.Encoding (decodeUtf8)
 import Data.Text.Lazy qualified as LazyText
 import GHC.Exts (IsString (..))
 import GHC.TypeLits (KnownSymbol, symbolVal)
 import Prettyprinter (Pretty, pretty)
+import System.Log.FastLogger (FormattedTime)
+import UnliftIO (MonadUnliftIO)
 
 import Booster.Definition.Attributes.Base
 import Booster.Definition.Base (RewriteRule (..), SourceRef (..), sourceRef)
@@ -44,11 +49,10 @@ 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.JsonRpc.Types.ContextLog as CL
 import Kore.Util (showHashHex)
-import System.Log.FastLogger (FormattedTime)
-import UnliftIO (MonadUnliftIO)
+
 
 newtype Logger a = Logger (a -> IO ())
 
@@ -56,13 +60,8 @@ class ToLogFormat a where
     toTextualLog :: a -> Text
     toJSONLog :: a -> Value
 
-data LogContext = forall a. ToLogFormat a => LogContext a
-
-instance IsString LogContext where
-    fromString = LogContext . pack
-
 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,18 +99,12 @@ logMessage' a =
 logPretty :: (LoggerMIO m, Pretty a) => a -> m ()
 logPretty = logMessage . renderOneLineText . pretty
 
-withContext :: LoggerMIO m => LogContext -> m a -> m a
+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
@@ -127,7 +120,7 @@ instance ToLogFormat Text where
     toJSONLog t = String t
 
 withTermContext :: LoggerMIO m => Term -> m a -> m a
-withTermContext t@(Term attrs _) m = withContext (LogContext $ TermCtxt attrs.hash) $ do
+withTermContext t@(Term attrs _) m = withContext (CLWithId $ CtxTerm $ Hex7 attrs.hash) $ do
     withContext "kore-term" $ logMessage t
     m
 
@@ -140,31 +133,17 @@ 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
+withKorePatternContext p m = withContext (CLWithId $ CtxTerm (Hex7 h)) $ do
+    withContext "kore-term" $ logMessage p
     m
+  where
+    h = Data.Hashable.hash (p.term, p.constraints, p.ceilConditions)
 
-withRuleContext :: KnownSymbol tag => LoggerMIO m => RewriteRule tag -> m a -> m a
-withRuleContext rule m = withContext (LogContext rule) $ do
+withRuleContext ::
+    (KnownSymbol tag, ContextFor (RewriteRule tag)) =>
+    LoggerMIO m => RewriteRule tag -> m a -> m a
+withRuleContext rule m = withContext (contextFor rule) $ do
     withContext "detail" $ logPretty $ case sourceRef rule of
         Located Location{file = FileSource f, position} ->
             Located
@@ -172,6 +151,21 @@ withRuleContext rule m = withContext (LogContext rule) $ do
         loc -> loc
     m
 
+class ContextFor a where
+    contextFor :: a -> CLContext
+
+instance ContextFor (RewriteRule "rewrite") where
+    contextFor = CLWithId . CtxRewrite . parseRuleId
+
+instance ContextFor (RewriteRule "function") where
+    contextFor = CLWithId . CtxFunction . parseRuleId
+
+instance ContextFor (RewriteRule "simplification") where
+    contextFor = CLWithId . CtxSimplification . parseRuleId
+
+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 +190,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 +204,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/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 0b43643400..1a8bbd1098 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -118,27 +118,31 @@ instance Show IdContext where
 
 ----------------------------------------
 data UniqueId
-    = Hex7 Integer -- short hashes (7 char)
+    = Hex7 Int -- short hashes (7 char)
     | Hex64 Integer -- long hashes (64 char)
     | UNKNOWN
     deriving stock (Generic, Eq, Ord)
 
 instance Show UniqueId where
     show (Hex7 i) = showHex i ""
-    show (Hex64 i) = showHex i "" -- or show shortened version?
+    show (Hex64 i) = showHex i ""
     show UNKNOWN = "UNKNOWN"
 
+parseUId :: Text -> Maybe UniqueId
+parseUId "UNKNOWN" = pure UNKNOWN
+parseUId hex =
+    case readHex $ unpack hex of
+        [(h, "")]
+            | Text.length hex < 8 -> Just $ Hex7 (fromIntegral h)
+            | Text.length hex <= 64 -> Just $ Hex64 h
+        _otherwise -> Nothing
+
 instance FromJSON UniqueId where
     parseJSON = JSON.withText "Hexadecimal Hash" parseHex
       where
         parseHex :: Text -> JSON.Parser UniqueId
-        parseHex "UNKNOWN" = pure UNKNOWN
         parseHex hex =
-            case readHex $ unpack hex of
-                [(h, "")]
-                    | Text.length hex < 8 -> pure $ Hex7 h
-                    | Text.length hex <= 64 -> pure $ Hex64 h
-                _otherwise -> JSON.parseFail $ "Bad hash value: " <> show hex
+            maybe (JSON.parseFail $ "Bad hash value: " <> show hex) pure $ parseUId hex
 
 instance ToJSON UniqueId where
     toJSON = \case

From 4c1ef281f8764720c130d628caa0e94ae33c254d Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 18 Jun 2024 22:15:35 +1000
Subject: [PATCH 04/16] Booster.Log type-checks, patterns for export

---
 booster/library/Booster/Log.hs                | 41 ++++++-------
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 59 +++++++++++++++++++
 2 files changed, 80 insertions(+), 20 deletions(-)

diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index 98add28cac..768d1e9389 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -17,21 +17,15 @@ 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.Encoding (decodeUtf8)
-import Data.Text.Lazy qualified as LazyText
-import GHC.Exts (IsString (..))
-import GHC.TypeLits (KnownSymbol, symbolVal)
 import Prettyprinter (Pretty, pretty)
 import System.Log.FastLogger (FormattedTime)
 import UnliftIO (MonadUnliftIO)
@@ -41,6 +35,7 @@ import Booster.Definition.Base (RewriteRule (..), SourceRef (..), sourceRef)
 import Booster.Pattern.Base (
     Pattern (..),
     Predicate (..),
+    Symbol (..),
     Term (..),
     TermAttributes (hash),
     pattern AndTerm,
@@ -51,8 +46,6 @@ import Booster.Syntax.Json.Externalise (externaliseTerm)
 import Booster.Util (Flag (..))
 import Kore.JsonRpc.Types (rpcJsonConfig)
 import Kore.JsonRpc.Types.ContextLog as CL
-import Kore.Util (showHashHex)
-
 
 newtype Logger a = Logger (a -> IO ())
 
@@ -60,6 +53,10 @@ class ToLogFormat a where
     toTextualLog :: a -> Text
     toJSONLog :: a -> Value
 
+instance ToLogFormat CLContext where
+    toTextualLog = pack . show
+    toJSONLog = toJSON
+
 data LogMessage where
     LogMessage :: ToLogFormat a => Flag "alwaysShown" -> [CLContext] -> a -> LogMessage
 
@@ -120,13 +117,13 @@ instance ToLogFormat Text where
     toJSONLog t = String t
 
 withTermContext :: LoggerMIO m => Term -> m a -> m a
-withTermContext t@(Term attrs _) m = withContext (CLWithId $ CtxTerm $ Hex7 attrs.hash) $ do
-    withContext "kore-term" $ logMessage t
+withTermContext t@(Term attrs _) m = withContext (CTerm $ Hex7 attrs.hash) $ do
+    withContext CKoreTerm $ 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
@@ -134,17 +131,18 @@ instance ToLogFormat KorePattern where
     toJSONLog p = toJSON p
 
 withKorePatternContext :: LoggerMIO m => KorePattern -> m a -> m a
-withKorePatternContext p m = withContext (CLWithId $ CtxTerm (Hex7 h)) $ do
-    withContext "kore-term" $ logMessage p
-    m
+withKorePatternContext p m =
+    withContext (CTerm (Hex7 h)) $ do
+        withContext CKoreTerm $ logMessage p
+        m
   where
-    h = Data.Hashable.hash (p.term, p.constraints, p.ceilConditions)
+    h = Data.Hashable.hash $ show p -- FIXME
 
 withRuleContext ::
-    (KnownSymbol tag, ContextFor (RewriteRule tag)) =>
+    ContextFor (RewriteRule tag) =>
     LoggerMIO m => RewriteRule tag -> m a -> m a
 withRuleContext rule m = withContext (contextFor rule) $ do
-    withContext "detail" $ logPretty $ case sourceRef rule of
+    withContext CDetail $ logPretty $ case sourceRef rule of
         Located Location{file = FileSource f, position} ->
             Located
                 Location{file = FileSource $ "..." <> (intercalate "/" $ takeEnd 3 $ splitOn "/" f), position}
@@ -155,13 +153,16 @@ class ContextFor a where
     contextFor :: a -> CLContext
 
 instance ContextFor (RewriteRule "rewrite") where
-    contextFor = CLWithId . CtxRewrite . parseRuleId
+    contextFor = CRewrite . parseRuleId
 
 instance ContextFor (RewriteRule "function") where
-    contextFor = CLWithId . CtxFunction . parseRuleId
+    contextFor = CFunction . parseRuleId
 
 instance ContextFor (RewriteRule "simplification") where
-    contextFor = CLWithId . CtxSimplification . parseRuleId
+    contextFor = CSimplification . parseRuleId
+
+instance ContextFor Symbol where
+    contextFor = CHook . (maybe "not-hooked" decodeUtf8) . (.attributes.hook)
 
 parseRuleId :: RewriteRule tag -> CL.UniqueId
 parseRuleId = fromMaybe CL.UNKNOWN . CL.parseUId . coerce . (.attributes.uniqueId)
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 1a8bbd1098..be7ad53644 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -Wno-partial-fields #-}
+{-# LANGUAGE PatternSynonyms #-}
 
 {- |
 Copyright   : (c) Runtime Verification, 2023
@@ -83,6 +84,49 @@ data SimpleContext
     | CtxInfo
     deriving stock (Generic, Data, Enum, Show, Eq, Ord)
 
+
+pattern CBooster :: CLContext
+pattern CBooster = CLNullary CtxBooster
+pattern CKore :: CLContext
+pattern CKore = CLNullary CtxKore
+pattern CProxy :: CLContext
+pattern CProxy = CLNullary CtxProxy
+    -- method
+pattern CExecute :: CLContext
+pattern CExecute = CLNullary CtxExecute
+pattern CSimplify :: CLContext
+pattern CSimplify = CLNullary CtxSimplify
+pattern CImplies :: CLContext
+pattern CImplies = CLNullary CtxImplies
+pattern CGetModel :: CLContext
+pattern CGetModel = CLNullary CtxGetModel
+    -- mode/phase
+pattern CMatch :: CLContext
+pattern CMatch = CLNullary CtxMatch
+pattern CDefinedness :: CLContext
+pattern CDefinedness = CLNullary CtxDefinedness
+pattern CConstraint :: CLContext
+pattern CConstraint = CLNullary CtxConstraint
+    -- results
+pattern CFailure :: CLContext
+pattern CFailure = CLNullary CtxFailure
+pattern CAbort :: CLContext
+pattern CAbort = CLNullary CtxAbort
+pattern CSuccess :: CLContext
+pattern CSuccess = CLNullary CtxSuccess
+    -- information
+pattern CKoreTerm :: CLContext
+pattern CKoreTerm = CLNullary CtxKoreTerm
+pattern CDetail :: CLContext
+pattern CDetail = CLNullary CtxDetail
+    -- standard log levels
+pattern CError :: CLContext
+pattern CError = CLNullary CtxError
+pattern CWarn :: CLContext
+pattern CWarn = CLNullary CtxWarn
+pattern CInfo :: CLContext
+pattern CInfo = CLNullary CtxInfo
+
 -- translation table for nullary constructors
 translateSimple :: [(SimpleContext, String)]
 translateSimple =
@@ -116,6 +160,21 @@ instance Show IdContext where
     show (CtxTerm uid) = "term " <> show uid
     show (CtxHook name) = "simplification " <> unpack name
 
+pattern CRewrite :: UniqueId -> CLContext
+pattern CRewrite u = CLWithId (CtxRewrite u)
+
+pattern CSimplification :: UniqueId -> CLContext
+pattern CSimplification u = CLWithId (CtxSimplification u)
+
+pattern CFunction :: UniqueId -> CLContext
+pattern CFunction u = CLWithId (CtxFunction u)
+
+pattern CTerm :: UniqueId -> CLContext
+pattern CTerm u = CLWithId (CtxTerm u)
+
+pattern CHook :: Text -> CLContext
+pattern CHook t = CLWithId (CtxHook t)
+
 ----------------------------------------
 data UniqueId
     = Hex7 Int -- short hashes (7 char)

From 9deaf228b97c825fbe52116f105950c7342d9504 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 19 Jun 2024 13:48:11 +1000
Subject: [PATCH 05/16] convert all logging call sites

---
 booster/library/Booster/JsonRpc.hs            | 44 +++++-----
 booster/library/Booster/Log.hs                | 81 ++++++++++++++-----
 .../library/Booster/Pattern/ApplyEquations.hs | 76 +++++++++--------
 booster/library/Booster/Pattern/Rewrite.hs    | 46 +++++------
 booster/library/Booster/SMT/Interface.hs      | 20 ++---
 booster/tools/booster/Proxy.hs                | 70 ++++++++--------
 booster/tools/booster/Server.hs               | 24 +++---
 dev-tools/booster-dev/Server.hs               |  4 +-
 dev-tools/kore-rpc-dev/Server.hs              |  8 +-
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 57 +++++++------
 10 files changed, 234 insertions(+), 196 deletions(-)

diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
index af5d228ecd..261eab2fe6 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 CExecute $ 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 CInternalise $ 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 CAddModule $ 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 CSimplify $ 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 CInternalise $ 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 CConstraint $
                             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 CGetModel $
                     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 CInternalise $ 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 CGetModel $
                                         logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
 
                                     unless (null unsupported) $ do
-                                        withContext "get-model" $ do
+                                        withContext CGetModel $ do
                                             logMessage' ("ignoring unsupported predicates" :: Text)
-                                            withContext "detail" $
+                                            withContext CDetail $
                                                 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 CGetModel $ do
                                             logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text)
-                                            withContext "detail" $
+                                            withContext CDetail $
                                                 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 CGetModel $
+                                        withContext CSMT $
                                             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 CGetModel $
+                            withContext CSMT $
                                 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 CImplies $ 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 CInternalise $ 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 CInternalise $ 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 CDetail $
                                 logMessage
                                     (Text.unwords $ map prettyPattern unsupportedL)
                         unless (null unsupportedR) $
-                            withContext "detail" $
+                            withContext CDetail $
                                 logMessage
                                     (Text.unwords $ map prettyPattern unsupportedR)
                     let
diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index 768d1e9389..134eb3da89 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -4,7 +4,44 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Booster.Log (module Booster.Log) where
+module Booster.Log (
+    module Booster.Log,
+    -- re-export all log context patterns for convenience
+    pattern CBooster,
+    pattern CKore,
+    pattern CProxy,
+    pattern CExecute,
+    pattern CSimplify,
+    pattern CImplies,
+    pattern CGetModel,
+    pattern CAddModule,
+    pattern CInternalise,
+    pattern CMatch,
+    pattern CDefinedness,
+    pattern CConstraint,
+    pattern CSMT,
+    pattern CLlvm,
+    pattern CCached,
+    pattern CFailure,
+    pattern CIndeterminate,
+    pattern CAbort,
+    pattern CSuccess,
+    pattern CBreak,
+    pattern CContinue,
+    pattern CKoreTerm,
+    pattern CDetail,
+    pattern CSubstitution,
+    pattern CDepth,
+    pattern CError,
+    pattern CWarn,
+    pattern CInfo,
+    pattern CRewrite,
+    pattern CSimplification,
+    pattern CFunction,
+    pattern CCeil,
+    pattern CTerm,
+    pattern CHook,
+) where
 
 import Control.Monad (when)
 import Control.Monad.IO.Class
@@ -57,6 +94,25 @@ 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 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" -> [CLContext] -> a -> LogMessage
 
@@ -102,20 +158,6 @@ withContext c =
         ( \(Logger l) -> Logger $ l . (\(LogMessage alwaysShown ctxt m) -> LogMessage alwaysShown (c : ctxt) m)
         )
 
-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 (CTerm $ Hex7 attrs.hash) $ do
     withContext CKoreTerm $ logMessage t
@@ -152,15 +194,18 @@ withRuleContext rule m = withContext (contextFor rule) $ do
 class ContextFor a where
     contextFor :: a -> CLContext
 
-instance ContextFor (RewriteRule "rewrite") where
+instance ContextFor (RewriteRule "Rewrite") where
     contextFor = CRewrite . parseRuleId
 
-instance ContextFor (RewriteRule "function") where
+instance ContextFor (RewriteRule "Function") where
     contextFor = CFunction . parseRuleId
 
-instance ContextFor (RewriteRule "simplification") where
+instance ContextFor (RewriteRule "Simplification") where
     contextFor = CSimplification . parseRuleId
 
+instance ContextFor (RewriteRule "Ceil") where
+    contextFor = CCeil . parseRuleId
+
 instance ContextFor Symbol where
     contextFor = CHook . (maybe "not-hooked" decodeUtf8) . (.attributes.hook)
 
diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index 8c110f003b..0a2b0abfbe 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 CAbort $
                 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 CWarn $
         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 CAbort $ do
             logWarn "Equation loop detected."
-            withContext "detail" $
+            withContext CDetail $
                 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 CAbort $ 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 CAbort $ do
                     logWarn $
                         renderOneLineText $
                             "Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
-                    withContext "detail" . logMessage . renderOneLineText $
+                    withContext CDetail . 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 CLlvm $ do
             LLVM.simplifyTerm api definition t (sortOfTerm t)
                 >>= \case
                     Left (LlvmError e) -> do
-                        withContext "abort" $
+                        withContext CAbort $
                             logWarn $
                                 "LLVM backend error detected: " <> Text.decodeUtf8 e
                         throw $ UndefinedTerm t $ LlvmError e
                     Right result -> do
                         when (result /= t) $ do
                             setChanged
-                            withContext "success" $
+                            withContext CSuccess $
                                 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 CSuccess $
+                        withContext CCached $
                             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 CAbort $
                                 logWarn e
                             throw (InternalError e)
-                    withContext (LogContext $ HookCtxt hookName) $
+                    withContext (contextFor 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 CFailure (logMessage ("Hook returned no result" :: Text)) >> pure Nothing
     checkChanged (Just t) =
-        withContext "success" $ withTermContext t $ do
+        withContext CSuccess $ 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 CAbort $
             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 CAbort $
             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 CAbort $ 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 >> (withContext (contextFor eq) $ withContext CSuccess $ withTermContext t $ pure t)
             Left (m, err) ->
                 handler
-                    ( ( withContext (LogContext eq) $
+                    ( ( withContext (contextFor eq) $
                             m $
-                                withContext "failure" . withContext "continue"
+                                withContext CFailure . withContext CContinue
                       )
                         >> processEquations rest
                     )
-                    ( ( withContext (LogContext eq) $
+                    ( ( withContext (contextFor eq) $
                             m $
-                                withContext "failure" . withContext "break"
+                                withContext CFailure . withContext CBreak
                       )
                         >> 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 CAbort $
             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 CMatch $
                         ctxt $
                             logPretty failReason
                 , FailedMatch failReason
@@ -743,7 +741,7 @@ applyEquation term rule = runExceptT $ do
         MatchIndeterminate remainder ->
             throwE
                 ( \ctxt ->
-                    withContext "match" $
+                    withContext CMatch $
                         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 CMatch $ checkConcreteness rule.attributes.concreteness subst
 
-            withContext "match" $ withContext "success" $ do
+            withContext CMatch $ withContext CSuccess $ do
                 logMessage rule
-                withContext "substitution"
+                withContext CSubstitution
                     $ 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 CConstraint $ 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 CLlvm $
                         LLVM.simplifyBool api t >>= \case
                             Left (LlvmError e) -> do
-                                withContext "abort" $
+                                withContext CAbort $
                                     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 CSuccess $
                                     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..c8e7faa23a 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 CMatch $ case matchTerms Rewrite def rule.lhs pat.term of
         MatchFailed (SubsortingError sortError) -> do
-            withContext "error" $ logPretty sortError
+            withContext CError $ logPretty sortError
             failRewrite $ RewriteSortError rule pat.term sortError
         MatchFailed err@ArgLengthsDiffer{} -> do
-            withContext "error" $ logPretty err
+            withContext CError $ logPretty err
             failRewrite $ InternalMatchError $ renderText $ pretty err
         MatchFailed reason -> do
-            withContext "failure" $ logPretty reason
+            withContext CFailure $ logPretty reason
             fail "Rule matching failed"
         MatchIndeterminate remainder -> do
-            withContext "indeterminate" $
+            withContext CIndeterminate $
                 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 CSuccess $ do
                 logMessage rule
-                withContext "substitution"
+                withContext CSubstitution
                     $ 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 CDefinedness . withContext CAbort $
             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 CConstraint . withContext CAbort . 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 CFailure $ 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 CConstraint . withContext CAbort $
                     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 CSuccess $ 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 CSuccess $
         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 CConstraint $
                 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 CDepth . 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 CSimplify $ 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 CMatch . withContext CAbort . 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..e4901081b0 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.CSMT $ 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
-        Log.logMessage ("No constraints or substitutions to check, returning Sat" :: Text)
+    | null ps && Map.null subst = Log.withContext Log.CSMT $ 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.CSMT $ do
         Log.logMessage $ "SMT translation error: " <> errMsg
         smtTranslateError errMsg
-    | Right (smtAsserts, transState) <- translated = Log.withContext "smt" $ do
+    | Right (smtAsserts, transState) <- translated = Log.withContext Log.CSMT $ 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.CSMT $ do
+        Log.withContext Log.CAbort $ 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.CSMT $ 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.CAbort $
                     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.CAbort $ 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..279e7127d1 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 CProxy $
                         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 CProxy $
                         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 CProxy $
+                            Booster.Log.withContext CAbort $
                                 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 CProxy $
+                            Booster.Log.withContext CAbort $
                                 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 CProxy $
+                                Booster.Log.withContext CAbort $
+                                    Booster.Log.withContext CDetail $
                                         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 CProxy $
                     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 CProxy $
             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 CProxy $
                 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 CProxy $
             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 CProxy $
                         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 CProxy $
                                 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 CProxy $
                         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 CProxy $
                         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 CProxy $
                                 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 CProxy $
                                 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 CProxy $
                                     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 CProxy $
+                                                Booster.Log.withContext CAbort $
                                                     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 CProxy $
+                                                    Booster.Log.withContext CAbort $
                                                         Booster.Log.logMessage $
                                                             "Booster and kore disagree: " <> Text.pack (show (bRes, kRes))
                                             | otherwise ->
-                                                Booster.Log.withContext "proxy" $
-                                                    Booster.Log.withContext "abort" $
+                                                Booster.Log.withContext CProxy $
+                                                    Booster.Log.withContext CAbort $
                                                         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 CProxy $
                                                 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 CProxy . 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 CProxy . Booster.Log.logMessage . Text.pack $
                         "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth
                     -- perform post-exec simplification
                     postExecResult <-
@@ -543,7 +543,7 @@ 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 CProxy . Booster.Log.logMessage . Text.pack $ "Simplifying execution state"
             simplResult <-
                 handleSimplify (toSimplifyRequest s) Nothing
             case simplResult of
@@ -576,13 +576,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 CProxy . 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 CProxy . Booster.Log.logMessage . Text.pack $
                         "Unexpected failure when calling Kore simplifier, returning original term"
                     pure $ Right (s, Nothing)
           where
@@ -606,13 +606,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 CProxy . 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 CProxy . 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 ac19dfe651..9fb2e87c93 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 CProxy $
                 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 CProxy $
                             Booster.Log.logMessage' $
                                 "Main module " <> mainModuleName <> " not found in " <> Text.pack definitionFile
                     liftIO exitFailure
 
                 liftIO $
                     runBoosterLogger $
-                        Booster.Log.withContext "ceil" $
+                        Booster.Log.withContext CInfo $ -- 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 CInfo -- 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 CInfo -- 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 CInfo -- 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 CProxy $
                         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 CBooster
                             . Booster.respond boosterState
 
                     proxyConfig =
@@ -341,7 +341,7 @@ main = do
                             , handleSomeException
                             ]
                     interruptHandler _ =
-                        runBoosterLogger . Booster.Log.withContext "proxy" $ do
+                        runBoosterLogger . Booster.Log.withContext CProxy $ 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 CProxy $
             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..b0999fa8bc 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.CBooster
                         . respond stateVar
                 )
                 [handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException]
diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs
index f6914b620b..cb9985ed78 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 CKore $
                     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 CKore $
             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 CKore $
                         Booster.Log.logMessage' ("Starting RPC server" :: Text.Text)
 
                 let koreRespond :: Respond (API 'Req) (LoggerT IO) (API 'Res)
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index be7ad53644..290a2d05be 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -67,17 +67,27 @@ data SimpleContext
     | 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
@@ -85,46 +95,44 @@ data SimpleContext
     deriving stock (Generic, Data, Enum, Show, Eq, Ord)
 
 
-pattern CBooster :: CLContext
+pattern CBooster, CKore, CProxy :: CLContext
 pattern CBooster = CLNullary CtxBooster
-pattern CKore :: CLContext
 pattern CKore = CLNullary CtxKore
-pattern CProxy :: CLContext
 pattern CProxy = CLNullary CtxProxy
     -- method
-pattern CExecute :: CLContext
+pattern CExecute, CSimplify, CImplies, CGetModel, CAddModule :: CLContext
 pattern CExecute = CLNullary CtxExecute
-pattern CSimplify :: CLContext
 pattern CSimplify = CLNullary CtxSimplify
-pattern CImplies :: CLContext
 pattern CImplies = CLNullary CtxImplies
-pattern CGetModel :: CLContext
 pattern CGetModel = CLNullary CtxGetModel
+pattern CAddModule = CLNullary CtxAddModule
     -- mode/phase
-pattern CMatch :: CLContext
+pattern CInternalise, CMatch, CDefinedness, CConstraint, CSMT, CLlvm, CCached :: CLContext
+pattern CInternalise = CLNullary CtxInternalise
 pattern CMatch = CLNullary CtxMatch
-pattern CDefinedness :: CLContext
 pattern CDefinedness = CLNullary CtxDefinedness
-pattern CConstraint :: CLContext
 pattern CConstraint = CLNullary CtxConstraint
+pattern CSMT = CLNullary CtxSMT
+pattern CLlvm = CLNullary CtxLlvm
+pattern CCached = CLNullary CtxCached
     -- results
-pattern CFailure :: CLContext
+pattern CFailure, CIndeterminate, CAbort, CSuccess, CBreak, CContinue :: CLContext
 pattern CFailure = CLNullary CtxFailure
-pattern CAbort :: CLContext
+pattern CIndeterminate = CLNullary CtxIndeterminate
 pattern CAbort = CLNullary CtxAbort
-pattern CSuccess :: CLContext
 pattern CSuccess = CLNullary CtxSuccess
+pattern CBreak = CLNullary CtxBreak
+pattern CContinue = CLNullary CtxContinue
     -- information
-pattern CKoreTerm :: CLContext
+pattern CKoreTerm, CDetail, CSubstitution, CDepth :: CLContext
 pattern CKoreTerm = CLNullary CtxKoreTerm
-pattern CDetail :: CLContext
 pattern CDetail = CLNullary CtxDetail
-    -- standard log levels
-pattern CError :: CLContext
+pattern CSubstitution = CLNullary CtxSubstitution
+pattern CDepth = CLNullary CtxDepth
+   -- standard log levels
+pattern CError, CWarn, CInfo :: CLContext
 pattern CError = CLNullary CtxError
-pattern CWarn :: CLContext
 pattern CWarn = CLNullary CtxWarn
-pattern CInfo :: CLContext
 pattern CInfo = CLNullary CtxInfo
 
 -- translation table for nullary constructors
@@ -146,6 +154,7 @@ data IdContext
       CtxRewrite UniqueId
     | CtxSimplification UniqueId
     | CtxFunction UniqueId
+    | CtxCeil UniqueId
     | CtxTerm UniqueId
     -- entities with name
     | CtxHook Text
@@ -157,19 +166,15 @@ 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) = "simplification " <> unpack name
 
-pattern CRewrite :: UniqueId -> CLContext
+pattern CRewrite, CSimplification, CFunction, CCeil, CTerm :: UniqueId -> CLContext
 pattern CRewrite u = CLWithId (CtxRewrite u)
-
-pattern CSimplification :: UniqueId -> CLContext
 pattern CSimplification u = CLWithId (CtxSimplification u)
-
-pattern CFunction :: UniqueId -> CLContext
 pattern CFunction u = CLWithId (CtxFunction u)
-
-pattern CTerm :: UniqueId -> CLContext
+pattern CCeil u = CLWithId (CtxCeil u)
 pattern CTerm u = CLWithId (CtxTerm u)
 
 pattern CHook :: Text -> CLContext

From 2fc8bc91dce9337c4cf15b95e8f969e06b137726 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 19 Jun 2024 13:52:23 +1000
Subject: [PATCH 06/16] formatting

---
 booster/library/Booster/Log.hs                | 16 +++--
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 64 ++++++++++---------
 2 files changed, 43 insertions(+), 37 deletions(-)

diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index 134eb3da89..474ed26ff7 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -107,11 +107,12 @@ instance ToLogFormat (RewriteRule tag) where
     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
+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" -> [CLContext] -> a -> LogMessage
@@ -182,7 +183,10 @@ withKorePatternContext p m =
 
 withRuleContext ::
     ContextFor (RewriteRule tag) =>
-    LoggerMIO m => RewriteRule tag -> m a -> m a
+    LoggerMIO m =>
+    RewriteRule tag ->
+    m a ->
+    m a
 withRuleContext rule m = withContext (contextFor rule) $ do
     withContext CDetail $ logPretty $ case sourceRef rule of
         Located Location{file = FileSource f, position} ->
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 290a2d05be..807e01b8c2 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -1,5 +1,5 @@
-{-# OPTIONS_GHC -Wno-partial-fields #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# OPTIONS_GHC -Wno-partial-fields #-}
 
 {- |
 Copyright   : (c) Runtime Verification, 2023
@@ -48,10 +48,10 @@ instance FromJSON CLContext where
 options :: JSON.Options
 options =
     JSON.defaultOptions
-    { JSON.sumEncoding = JSON.ObjectWithSingleField
-    , JSON.constructorTagModifier = toJsonName
-    , JSON.allNullaryToStringTag = True
-    }
+        { JSON.sumEncoding = JSON.ObjectWithSingleField
+        , JSON.constructorTagModifier = toJsonName
+        , JSON.allNullaryToStringTag = True
+        }
 
 toJsonName :: String -> String
 toJsonName name = JSON.camelTo2 '-' $ fromMaybe name $ stripPrefix "Ctx" name
@@ -62,51 +62,52 @@ data SimpleContext
       CtxBooster
     | CtxKore
     | CtxProxy
-    -- method
-    | CtxExecute
+    | -- method
+      CtxExecute
     | CtxSimplify
     | CtxImplies
     | CtxGetModel
     | CtxAddModule
-    -- mode/phase
-    | CtxInternalise
+    | -- mode/phase
+      CtxInternalise
     | CtxMatch
     | CtxDefinedness
     | CtxConstraint
     | CtxSMT
     | CtxLlvm
     | CtxCached
-    -- results
-    | CtxFailure
+    | -- results
+      CtxFailure
     | CtxIndeterminate
     | CtxAbort
     | CtxSuccess
     | CtxBreak
     | CtxContinue
-    -- information
-    | CtxKoreTerm
+    | -- information
+      CtxKoreTerm
     | CtxDetail
     | CtxSubstitution
     | CtxDepth
-    -- standard log levels
-    | CtxError
+    | -- standard log levels
+      CtxError
     | CtxWarn
     | CtxInfo
     deriving stock (Generic, Data, Enum, Show, Eq, Ord)
 
-
 pattern CBooster, CKore, CProxy :: CLContext
 pattern CBooster = CLNullary CtxBooster
 pattern CKore = CLNullary CtxKore
 pattern CProxy = CLNullary CtxProxy
-    -- method
+
+-- method
 pattern CExecute, CSimplify, CImplies, CGetModel, CAddModule :: CLContext
 pattern CExecute = CLNullary CtxExecute
 pattern CSimplify = CLNullary CtxSimplify
 pattern CImplies = CLNullary CtxImplies
 pattern CGetModel = CLNullary CtxGetModel
 pattern CAddModule = CLNullary CtxAddModule
-    -- mode/phase
+
+-- mode/phase
 pattern CInternalise, CMatch, CDefinedness, CConstraint, CSMT, CLlvm, CCached :: CLContext
 pattern CInternalise = CLNullary CtxInternalise
 pattern CMatch = CLNullary CtxMatch
@@ -115,7 +116,8 @@ pattern CConstraint = CLNullary CtxConstraint
 pattern CSMT = CLNullary CtxSMT
 pattern CLlvm = CLNullary CtxLlvm
 pattern CCached = CLNullary CtxCached
-    -- results
+
+-- results
 pattern CFailure, CIndeterminate, CAbort, CSuccess, CBreak, CContinue :: CLContext
 pattern CFailure = CLNullary CtxFailure
 pattern CIndeterminate = CLNullary CtxIndeterminate
@@ -123,13 +125,15 @@ pattern CAbort = CLNullary CtxAbort
 pattern CSuccess = CLNullary CtxSuccess
 pattern CBreak = CLNullary CtxBreak
 pattern CContinue = CLNullary CtxContinue
-    -- information
+
+-- information
 pattern CKoreTerm, CDetail, CSubstitution, CDepth :: CLContext
 pattern CKoreTerm = CLNullary CtxKoreTerm
 pattern CDetail = CLNullary CtxDetail
 pattern CSubstitution = CLNullary CtxSubstitution
 pattern CDepth = CLNullary CtxDepth
-   -- standard log levels
+
+-- standard log levels
 pattern CError, CWarn, CInfo :: CLContext
 pattern CError = CLNullary CtxError
 pattern CWarn = CLNullary CtxWarn
@@ -156,8 +160,8 @@ data IdContext
     | CtxFunction UniqueId
     | CtxCeil UniqueId
     | CtxTerm UniqueId
-    -- entities with name
-    | CtxHook Text
+    | -- entities with name
+      CtxHook Text
     deriving stock (Generic, Eq)
 
 -- To/FromJSON by way of Generic
@@ -217,22 +221,20 @@ instance ToJSON UniqueId where
         UNKNOWN ->
             JSON.String "UNKNOWN"
       where
-          pad0 l = Text.takeEnd l . (Text.replicate l "0" <>)
-
+        pad0 l = Text.takeEnd l . (Text.replicate l "0" <>)
 
 ----------------------------------------
-data LogLine
-    = LogLine
-      { context :: [CLContext]
-      , message :: CLMessage
-      }
+data LogLine = LogLine
+    { context :: [CLContext]
+    , message :: CLMessage
+    }
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)
         via CustomJSON '[] LogLine
 
 data CLMessage
-    = CLText Text  -- generic log message
+    = CLText Text -- generic log message
     | CLValue JSON.Value -- other stuff
     deriving stock (Generic, Eq)
 

From c9677c4fd11b0412c07b3514a7a85e2f8e7435cd Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 19 Jun 2024 16:41:24 +1000
Subject: [PATCH 07/16] Make UniqueId carry text instead of a number

---
 booster/library/Booster/Log.hs                | 13 ++++---
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 34 +++++++------------
 2 files changed, 22 insertions(+), 25 deletions(-)

diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index 474ed26ff7..32cb6040b1 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -83,6 +83,7 @@ import Booster.Syntax.Json.Externalise (externaliseTerm)
 import Booster.Util (Flag (..))
 import Kore.JsonRpc.Types (rpcJsonConfig)
 import Kore.JsonRpc.Types.ContextLog as CL
+import Kore.Util
 
 newtype Logger a = Logger (a -> IO ())
 
@@ -160,7 +161,7 @@ withContext c =
         )
 
 withTermContext :: LoggerMIO m => Term -> m a -> m a
-withTermContext t@(Term attrs _) m = withContext (CTerm $ Hex7 attrs.hash) $ do
+withTermContext t@(Term attrs _) m = withContext (CTerm $ ShortId $ showHashHex attrs.hash) $ do
     withContext CKoreTerm $ logMessage t
     m
 
@@ -175,11 +176,9 @@ instance ToLogFormat KorePattern where
 
 withKorePatternContext :: LoggerMIO m => KorePattern -> m a -> m a
 withKorePatternContext p m =
-    withContext (CTerm (Hex7 h)) $ do
+    withContext (contextFor p) $ do
         withContext CKoreTerm $ logMessage p
         m
-  where
-    h = Data.Hashable.hash $ show p -- FIXME
 
 withRuleContext ::
     ContextFor (RewriteRule tag) =>
@@ -198,6 +197,12 @@ withRuleContext rule m = withContext (contextFor rule) $ do
 class ContextFor a where
     contextFor :: a -> CLContext
 
+instance ContextFor Term where
+    contextFor (Term attrs _) = CTerm . ShortId $ showHashHex attrs.hash
+
+instance ContextFor KorePattern where
+    contextFor = CTerm . ShortId . showHashHex . Data.Hashable.hash . show -- FIXME
+
 instance ContextFor (RewriteRule "Rewrite") where
     contextFor = CRewrite . parseRuleId
 
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 807e01b8c2..720c51ec3c 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -20,7 +20,6 @@ import Data.Text (Text, pack, unpack)
 import Data.Text qualified as Text
 import Data.Tuple (swap)
 import Deriving.Aeson
-import Numeric
 
 data CLContext
     = CLNullary SimpleContext
@@ -186,42 +185,35 @@ pattern CHook t = CLWithId (CtxHook t)
 
 ----------------------------------------
 data UniqueId
-    = Hex7 Int -- short hashes (7 char)
-    | Hex64 Integer -- long hashes (64 char)
+    = ShortId Text -- short hashes (7 char)
+    | LongId Text -- long hashes (64 char)
     | UNKNOWN
     deriving stock (Generic, Eq, Ord)
 
 instance Show UniqueId where
-    show (Hex7 i) = showHex i ""
-    show (Hex64 i) = showHex i ""
+    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 =
-    case readHex $ unpack hex of
-        [(h, "")]
-            | Text.length hex < 8 -> Just $ Hex7 (fromIntegral h)
-            | Text.length hex <= 64 -> Just $ Hex64 h
-        _otherwise -> Nothing
+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 "Hexadecimal Hash" parseHex
+    parseJSON = JSON.withText "Hash ID" parseHex
       where
         parseHex :: Text -> JSON.Parser UniqueId
         parseHex hex =
-            maybe (JSON.parseFail $ "Bad hash value: " <> show hex) pure $ parseUId hex
+            maybe (JSON.parseFail $ "Bad hash ID: " <> show hex) pure $ parseUId hex
 
 instance ToJSON UniqueId where
     toJSON = \case
-        Hex7 x ->
-            JSON.String . pad0 7 . pack $ showHex x ""
-        Hex64 x ->
-            JSON.String . pad0 64 . pack $ showHex x ""
-        UNKNOWN ->
-            JSON.String "UNKNOWN"
-      where
-        pad0 l = Text.takeEnd l . (Text.replicate l "0" <>)
+        ShortId x -> JSON.String x
+        LongId x -> JSON.String x
+        UNKNOWN -> JSON.String "UNKNOWN"
 
 ----------------------------------------
 data LogLine = LogLine

From 5e809675d6bbcae769a9b14216179ff7ab8d7a35 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 19 Jun 2024 16:56:24 +1000
Subject: [PATCH 08/16] add hook-related lines to expected output for
 log-simplify-json test

---
 .../simplify-log.txt.golden                   | 30 +++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
index 9d0628ae6e..0a8fee5466 100644
--- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
+++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
@@ -5,42 +5,72 @@
 {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"}
 {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\")"}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"80d934c"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} \"$n\""}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"5875655"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"4a555cf"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f2fa0db"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"5a046bd"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f464178"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"5a046bd"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f464178"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"9893c04"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"5b84449"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(VarN:SortInt{}, \"0\")"}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=Int_(VarN:SortInt{}, \"0\"))"}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]]}}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k :  (24, 10)"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"8f1e2b8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}}}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
+{"context":["booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
 {"context":["kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
+{"context":["booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","simplify",{"term":"66aa67b"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]]}}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k :  (24, 10)"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"Eq#VarA","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"EVar","name":"Eq#VarB","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]]}}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k :  (23, 10)"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"success",{"term":"f6384ee"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}}}
+{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
+{"context":["booster","simplify",{"term":"931632b"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["proxy"],"message":"Server shutting down"}

From a52f5055cc433e0e35c9ecd1a8e39e8b7294f413 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 19 Jun 2024 17:28:08 +1000
Subject: [PATCH 09/16] Refactoring to get rid of the patterns

---
 booster/library/Booster/JsonRpc.hs            |  44 ++++----
 booster/library/Booster/Log.hs                | 101 +++++++++---------
 .../library/Booster/Pattern/ApplyEquations.hs |  68 ++++++------
 booster/library/Booster/Pattern/Rewrite.hs    |  34 +++---
 booster/library/Booster/SMT/Interface.hs      |  18 ++--
 booster/tools/booster/Proxy.hs                |  69 ++++++------
 booster/tools/booster/Server.hs               |  20 ++--
 dev-tools/booster-dev/Server.hs               |   2 +-
 dev-tools/kore-rpc-dev/Server.hs              |   6 +-
 .../src/Kore/JsonRpc/Types/ContextLog.hs      |  60 +----------
 10 files changed, 180 insertions(+), 242 deletions(-)

diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
index 261eab2fe6..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 CExecute $ 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 CInternalise $ 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 CAddModule $ 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 CSimplify $ 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 CInternalise $ 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 CConstraint $
+                        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 CGetModel $
+                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 CInternalise $ 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 CGetModel $
+                                    withContext CtxGetModel $
                                         logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
 
                                     unless (null unsupported) $ do
-                                        withContext CGetModel $ do
+                                        withContext CtxGetModel $ do
                                             logMessage' ("ignoring unsupported predicates" :: Text)
-                                            withContext CDetail $
+                                            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 CGetModel $ do
+                                        withContext CtxGetModel $ do
                                             logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text)
-                                            withContext CDetail $
+                                            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 CGetModel $
-                                        withContext CSMT $
+                                    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 CGetModel $
-                            withContext CSMT $
+                        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 CImplies $ 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 CInternalise $ 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 CInternalise $ 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 CDetail $
+                            withContext CtxDetail $
                                 logMessage
                                     (Text.unwords $ map prettyPattern unsupportedL)
                         unless (null unsupportedR) $
-                            withContext CDetail $
+                            withContext CtxDetail $
                                 logMessage
                                     (Text.unwords $ map prettyPattern unsupportedR)
                     let
diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index 32cb6040b1..82204a97e6 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -5,42 +5,26 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 module Booster.Log (
-    module Booster.Log,
-    -- re-export all log context patterns for convenience
-    pattern CBooster,
-    pattern CKore,
-    pattern CProxy,
-    pattern CExecute,
-    pattern CSimplify,
-    pattern CImplies,
-    pattern CGetModel,
-    pattern CAddModule,
-    pattern CInternalise,
-    pattern CMatch,
-    pattern CDefinedness,
-    pattern CConstraint,
-    pattern CSMT,
-    pattern CLlvm,
-    pattern CCached,
-    pattern CFailure,
-    pattern CIndeterminate,
-    pattern CAbort,
-    pattern CSuccess,
-    pattern CBreak,
-    pattern CContinue,
-    pattern CKoreTerm,
-    pattern CDetail,
-    pattern CSubstitution,
-    pattern CDepth,
-    pattern CError,
-    pattern CWarn,
-    pattern CInfo,
-    pattern CRewrite,
-    pattern CSimplification,
-    pattern CFunction,
-    pattern CCeil,
-    pattern CTerm,
-    pattern CHook,
+    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)
@@ -154,16 +138,20 @@ logMessage' a =
 logPretty :: (LoggerMIO m, Pretty a) => a -> m ()
 logPretty = logMessage . renderOneLineText . pretty
 
-withContext :: LoggerMIO m => CLContext -> 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)
         )
 
 withTermContext :: LoggerMIO m => Term -> m a -> m a
-withTermContext t@(Term attrs _) m = withContext (CTerm $ ShortId $ showHashHex attrs.hash) $ do
-    withContext CKoreTerm $ 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 =
@@ -176,8 +164,8 @@ instance ToLogFormat KorePattern where
 
 withKorePatternContext :: LoggerMIO m => KorePattern -> m a -> m a
 withKorePatternContext p m =
-    withContext (contextFor p) $ do
-        withContext CKoreTerm $ logMessage p
+    withContextFor p $ do
+        withContext CtxKoreTerm $ logMessage p
         m
 
 withRuleContext ::
@@ -186,8 +174,8 @@ withRuleContext ::
     RewriteRule tag ->
     m a ->
     m a
-withRuleContext rule m = withContext (contextFor rule) $ do
-    withContext CDetail $ logPretty $ case sourceRef rule of
+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}
@@ -195,28 +183,35 @@ withRuleContext rule m = withContext (contextFor rule) $ do
     m
 
 class ContextFor a where
-    contextFor :: a -> CLContext
+    withContextFor :: LoggerMIO m => a -> m b -> m b
 
 instance ContextFor Term where
-    contextFor (Term attrs _) = CTerm . ShortId $ showHashHex attrs.hash
+    withContextFor (Term attrs _) =
+        withContext_ (CLWithId . CtxTerm . ShortId $ showHashHex attrs.hash)
 
 instance ContextFor KorePattern where
-    contextFor = CTerm . ShortId . showHashHex . Data.Hashable.hash . show -- FIXME
+    withContextFor p =
+        withContext_ (CLWithId . CtxTerm . ShortId . showHashHex . Data.Hashable.hash $ show p) -- FIXME
 
 instance ContextFor (RewriteRule "Rewrite") where
-    contextFor = CRewrite . parseRuleId
+    withContextFor r =
+        withContext_ (CLWithId . CtxRewrite $ parseRuleId r)
 
 instance ContextFor (RewriteRule "Function") where
-    contextFor = CFunction . parseRuleId
+    withContextFor r =
+        withContext_ (CLWithId . CtxFunction $ parseRuleId r)
 
 instance ContextFor (RewriteRule "Simplification") where
-    contextFor = CSimplification . parseRuleId
+    withContextFor r =
+        withContext_ (CLWithId . CtxSimplification $ parseRuleId r)
 
 instance ContextFor (RewriteRule "Ceil") where
-    contextFor = CCeil . parseRuleId
+    withContextFor r =
+        withContext_ (CLWithId . CtxCeil $ parseRuleId r)
 
 instance ContextFor Symbol where
-    contextFor = CHook . (maybe "not-hooked" decodeUtf8) . (.attributes.hook)
+    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)
diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index 0a2b0abfbe..367bf8e26f 100644
--- a/booster/library/Booster/Pattern/ApplyEquations.hs
+++ b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -218,7 +218,7 @@ popRecursion = do
     s <- getState
     if null s.recursionStack
         then do
-            withContext CAbort $
+            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 CWarn $
+    withContext CtxWarn $
         logMessage msg
 
 checkForLoop :: LoggerMIO io => Term -> EquationT io ()
 checkForLoop t = do
     EquationState{termStack} <- getState
     whenJust (Seq.elemIndexL t termStack) $ \i -> do
-        withContext CAbort $ do
+        withContext CtxAbort $ do
             logWarn "Equation loop detected."
-            withContext CDetail $
+            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 CAbort $ 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 CAbort $ do
+                withContext CtxAbort $ do
                     logWarn $
                         renderOneLineText $
                             "Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
-                    withContext CDetail . 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 CLlvm $ do
+        | isConcrete t && attributes.canBeEvaluated = withContext CtxLlvm $ do
             LLVM.simplifyTerm api definition t (sortOfTerm t)
                 >>= \case
                     Left (LlvmError e) -> do
-                        withContext CAbort $
+                        withContext CtxAbort $
                             logWarn $
                                 "LLVM backend error detected: " <> Text.decodeUtf8 e
                         throw $ UndefinedTerm t $ LlvmError e
                     Right result -> do
                         when (result /= t) $ do
                             setChanged
-                            withContext CSuccess $
+                            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 CSuccess $
-                        withContext CCached $
+                    withContext CtxSuccess $
+                        withContext CtxCached $
                             withTermContext cachedTerm $
                                 pure ()
                 pure cachedTerm
@@ -564,10 +564,10 @@ applyHooksAndEquations pref term = do
             SymbolApplication sym _sorts args
                 | Just hook <- flip Map.lookup Builtin.hooks =<< sym.attributes.hook -> do
                     let onError e = do
-                            withContext CAbort $
+                            withContext CtxAbort $
                                 logWarn e
                             throw (InternalError e)
-                    withContext (contextFor sym) $
+                    withContextFor sym $
                         either onError checkChanged $
                             runExcept (hook args)
             _other -> pure Nothing
@@ -576,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 CFailure (logMessage ("Hook returned no result" :: Text)) >> pure Nothing
+        withContext CtxFailure (logMessage ("Hook returned no result" :: Text)) >> pure Nothing
     checkChanged (Just t) =
-        withContext CSuccess $ withTermContext t $ do
+        withContext CtxSuccess $ withTermContext t $ do
             unless (t == term) setChanged
             pure (Just t)
 
@@ -620,7 +620,7 @@ handleFunctionEquation continue abort = \case
     IndeterminateCondition{} -> abort
     ConditionFalse _ -> continue
     EnsuresFalse p -> do
-        withContext CAbort $
+        withContext CtxAbort $
             logMessage ("A side condition was found to be false during evaluation (pruning)" :: Text)
         throw $ SideConditionFalse p
     RuleNotPreservingDefinedness -> abort
@@ -633,7 +633,7 @@ handleSimplificationEquation continue _abort = \case
     IndeterminateCondition{} -> continue
     ConditionFalse _ -> continue
     EnsuresFalse p -> do
-        withContext CAbort $
+        withContext CtxAbort $
             logMessage ("A side condition was found to be false during evaluation (pruning)" :: Text)
         throw $ SideConditionFalse p
     RuleNotPreservingDefinedness -> continue
@@ -650,7 +650,7 @@ applyEquations ::
 applyEquations theory handler term = do
     let index = Idx.termTopIndex term
     when (Idx.hasNone index) $ do
-        withContext CAbort $ logMessage ("Index 'None'" :: Text)
+        withContext CtxAbort $ logMessage ("Index 'None'" :: Text)
         throw (IndexIsNone term)
     let
         indexes = Set.toList $ Idx.coveringIndexes index
@@ -678,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 (contextFor eq) $ withContext CSuccess $ withTermContext t $ pure t)
+            Right t -> setChanged >> (withContextFor eq $ withContext CtxSuccess $ withTermContext t $ pure t)
             Left (m, err) ->
                 handler
-                    ( ( withContext (contextFor eq) $
+                    ( ( withContextFor eq $
                             m $
-                                withContext CFailure . withContext CContinue
+                                withContext CtxFailure . withContext CtxContinue
                       )
                         >> processEquations rest
                     )
-                    ( ( withContext (contextFor eq) $
+                    ( ( withContextFor eq $
                             m $
-                                withContext CFailure . withContext CBreak
+                                withContext CtxFailure . withContext CtxBreak
                       )
                         >> pure term
                     )
@@ -706,7 +706,7 @@ applyEquation ::
 applyEquation term rule = runExceptT $ do
     -- ensured by internalisation: no existentials in equations
     unless (null rule.existentials) $ do
-        withContext CAbort $
+        withContext CtxAbort $
             logMessage ("Equation with existentials" :: Text)
         lift . throw . InternalError $
             "Equation with existentials: " <> Text.pack (show rule)
@@ -733,7 +733,7 @@ applyEquation term rule = runExceptT $ do
         MatchFailed failReason ->
             throwE
                 ( \ctxt ->
-                    withContext CMatch $
+                    withContext CtxMatch $
                         ctxt $
                             logPretty failReason
                 , FailedMatch failReason
@@ -741,7 +741,7 @@ applyEquation term rule = runExceptT $ do
         MatchIndeterminate remainder ->
             throwE
                 ( \ctxt ->
-                    withContext CMatch $
+                    withContext CtxMatch $
                         ctxt $
                             logMessage $
                                 WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $
@@ -754,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 CMatch $ checkConcreteness rule.attributes.concreteness subst
+            withContext CtxMatch $ checkConcreteness rule.attributes.concreteness subst
 
-            withContext CMatch $ withContext CSuccess $ do
+            withContext CtxMatch $ withContext CtxSuccess $ do
                 logMessage rule
-                withContext CSubstitution
+                withContext CtxSubstitution
                     $ logMessage
                     $ WithJsonMessage
                         (object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList subst)])
@@ -827,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 CConstraint $ do
+    checkConstraint whenBottom (Predicate p) = withContext CtxConstraint $ do
         let fallBackToUnsimplifiedOrBottom :: EquationFailure -> EquationT io Term
             fallBackToUnsimplifiedOrBottom = \case
                 UndefinedTerm{} -> pure FalseBool
@@ -945,10 +945,10 @@ simplifyConstraint' recurseIntoEvalBool = \case
             mbApi <- (.llvmApi) <$> getConfig
             case mbApi of
                 Just api ->
-                    withContext CLlvm $
+                    withContext CtxLlvm $
                         LLVM.simplifyBool api t >>= \case
                             Left (LlvmError e) -> do
-                                withContext CAbort $
+                                withContext CtxAbort $
                                     logWarn $
                                         "LLVM backend error detected: " <> Text.decodeUtf8 e
                                 throw $ UndefinedTerm t $ LlvmError e
@@ -957,7 +957,7 @@ simplifyConstraint' recurseIntoEvalBool = \case
                                         if res
                                             then TrueBool
                                             else FalseBool
-                                withContext CSuccess $
+                                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 c8e7faa23a..ba37452c53 100644
--- a/booster/library/Booster/Pattern/Rewrite.hs
+++ b/booster/library/Booster/Pattern/Rewrite.hs
@@ -272,27 +272,27 @@ applyRule ::
 applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRuleAppT $ do
     def <- lift getDefinition
     -- unify terms
-    subst <- withContext CMatch $ 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 CError $ logPretty sortError
+            withContext CtxError $ logPretty sortError
             failRewrite $ RewriteSortError rule pat.term sortError
         MatchFailed err@ArgLengthsDiffer{} -> do
-            withContext CError $ logPretty err
+            withContext CtxError $ logPretty err
             failRewrite $ InternalMatchError $ renderText $ pretty err
         MatchFailed reason -> do
-            withContext CFailure $ logPretty reason
+            withContext CtxFailure $ logPretty reason
             fail "Rule matching failed"
         MatchIndeterminate remainder -> do
-            withContext CIndeterminate $
+            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 CSuccess $ do
+            withContext CtxSuccess $ do
                 logMessage rule
-                withContext CSubstitution
+                withContext CtxSubstitution
                     $ logMessage
                     $ WithJsonMessage
                         ( object
@@ -306,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 CDefinedness . withContext CAbort $
+        withContext CtxDefinedness . withContext CtxAbort $
             logMessage $
                 renderOneLineText $
                     "Uncertain about definedness of rule due to:"
@@ -337,7 +337,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
     mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask
 
     let smtUnclear = do
-            withContext CConstraint . withContext CAbort . logMessage . renderOneLineText $
+            withContext CtxConstraint . withContext CtxAbort . logMessage . renderOneLineText $
                 "Uncertain about condition(s) in a rule:" <+> pretty unclearRequires
             failRewrite $
                 RuleConditionUnclear rule . coerce . foldl1 AndTerm $
@@ -354,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 CFailure $ 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
@@ -362,7 +362,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                     smtUnclear -- no implication could be determined
         Nothing ->
             unless (null unclearRequires) $ do
-                withContext CConstraint . withContext CAbort $
+                withContext CtxConstraint . withContext CtxAbort $
                     logMessage $
                         renderOneLineText $
                             "Uncertain about a condition(s) in rule, no SMT solver:" <+> pretty unclearRequires
@@ -382,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 CSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
+                withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
                 RewriteRuleAppT $ pure Trivial
             Right _other ->
                 pure ()
@@ -413,7 +413,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                     <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints)
                 )
                 ceilConditions
-    withContext CSuccess $
+    withContext CtxSuccess $
         withPatternContext rewritten $
             return (rule, rewritten)
   where
@@ -428,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 CConstraint $
+            withContext CtxConstraint $
                 simplifyConstraint definition llvmApi smtSolver oldCache p
         -- update cache
         lift . RewriteT . lift . modify $ const cache
@@ -684,7 +684,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
         flip runStateT rewriteStart $ doSteps False pat
     pure (counter, traces, rr)
   where
-    logDepth = withContext CDepth . logMessage
+    logDepth = withContext CtxDepth . logMessage
 
     depthReached n = maybe False (n >=) mbMaxDepth
 
@@ -701,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 CSimplify $ do
+    simplifyP p = withContext CtxSimplify $ do
         st <- get
         let cache = st.simplifierCache
             smt = st.smtSolver
@@ -843,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 CMatch . withContext CAbort . 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 e4901081b0..12137371ca 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 Log.CSMT $ 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 Log.CSMT $ 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 Log.CSMT $ do
+    | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do
         Log.logMessage $ "SMT translation error: " <> errMsg
         smtTranslateError errMsg
-    | Right (smtAsserts, transState) <- translated = Log.withContext Log.CSMT $ 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 Log.CSMT $ do
-        Log.withContext Log.CAbort $ 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 Log.CSMT $ 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 Log.CAbort $
+                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 Log.CAbort $ 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 279e7127d1..b490df12d2 100644
--- a/booster/tools/booster/Proxy.hs
+++ b/booster/tools/booster/Proxy.hs
@@ -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 CProxy $
+                    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 CProxy $
+                    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 CProxy $
-                            Booster.Log.withContext CAbort $
+                        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 CProxy $
-                            Booster.Log.withContext CAbort $
+                        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 CProxy $
-                                Booster.Log.withContext CAbort $
-                                    Booster.Log.withContext CDetail $
+                            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 CProxy $
+                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 CProxy $
+        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 CProxy $
+            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 CProxy $
+        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 CProxy $
+                    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 CProxy $
+                            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 CProxy $
+                    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 CProxy $
+                    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 CProxy $
+                            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 CProxy $
+                            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 CProxy $
+                                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 CProxy $
-                                                Booster.Log.withContext CAbort $
+                                            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 CProxy $
-                                                    Booster.Log.withContext CAbort $
+                                                Booster.Log.withContext CtxProxy $
+                                                    Booster.Log.withContext CtxAbort $
                                                         Booster.Log.logMessage $
                                                             "Booster and kore disagree: " <> Text.pack (show (bRes, kRes))
                                             | otherwise ->
-                                                Booster.Log.withContext CProxy $
-                                                    Booster.Log.withContext CAbort $
+                                                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 CProxy $
+                                            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 CProxy . 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 CProxy . 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 CProxy . 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 CProxy . 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 CProxy . 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 CProxy . 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 CProxy . 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 9fb2e87c93..b36ee6899d 100644
--- a/booster/tools/booster/Server.hs
+++ b/booster/tools/booster/Server.hs
@@ -209,7 +209,7 @@ main = do
                         (fromMaybe stderrLogger mFileLogger)
 
         runBoosterLogger $
-            Booster.Log.withContext CProxy $
+            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 CProxy $
+                        Booster.Log.withContext CtxProxy $
                             Booster.Log.logMessage' $
                                 "Main module " <> mainModuleName <> " not found in " <> Text.pack definitionFile
                     liftIO exitFailure
 
                 liftIO $
                     runBoosterLogger $
-                        Booster.Log.withContext CInfo $ -- FIXME "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 CInfo -- FIXME "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 CInfo -- FIXME"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 CInfo -- FIXME"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 CProxy $
+                    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 CBooster
+                        Booster.Log.withContext CtxBooster
                             . Booster.respond boosterState
 
                     proxyConfig =
@@ -341,7 +341,7 @@ main = do
                             , handleSomeException
                             ]
                     interruptHandler _ =
-                        runBoosterLogger . Booster.Log.withContext CProxy $ 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 CProxy $
+        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 b0999fa8bc..abb3855b7c 100644
--- a/dev-tools/booster-dev/Server.hs
+++ b/dev-tools/booster-dev/Server.hs
@@ -161,7 +161,7 @@ runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLev
                 ( const $
                     flip runReaderT filteredBoosterContextLogger
                         . Booster.Log.unLoggerT
-                        . Booster.Log.withContext Booster.Log.CBooster
+                        . Booster.Log.withContext Booster.Log.CtxBooster
                         . respond stateVar
                 )
                 [handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException]
diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs
index cb9985ed78..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 CKore $
+                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 CKore $
+        withContext CtxKore $
             logMessage' $
                 Text.pack $
                     show method <> " (using kore)"
@@ -230,7 +230,7 @@ main = do
                 kore@KoreServer{runSMT} <-
                     mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions
                 runBoosterLogger $
-                    Booster.Log.withContext CKore $
+                    Booster.Log.withContext CtxKore $
                         Booster.Log.logMessage' ("Starting RPC server" :: Text.Text)
 
                 let koreRespond :: Respond (API 'Req) (LoggerT IO) (API 'Res)
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 720c51ec3c..fc4b649f25 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# OPTIONS_GHC -Wno-partial-fields #-}
-
 {- |
 Copyright   : (c) Runtime Verification, 2023
 License     : BSD-3-Clause
@@ -93,51 +90,6 @@ data SimpleContext
     | CtxInfo
     deriving stock (Generic, Data, Enum, Show, Eq, Ord)
 
-pattern CBooster, CKore, CProxy :: CLContext
-pattern CBooster = CLNullary CtxBooster
-pattern CKore = CLNullary CtxKore
-pattern CProxy = CLNullary CtxProxy
-
--- method
-pattern CExecute, CSimplify, CImplies, CGetModel, CAddModule :: CLContext
-pattern CExecute = CLNullary CtxExecute
-pattern CSimplify = CLNullary CtxSimplify
-pattern CImplies = CLNullary CtxImplies
-pattern CGetModel = CLNullary CtxGetModel
-pattern CAddModule = CLNullary CtxAddModule
-
--- mode/phase
-pattern CInternalise, CMatch, CDefinedness, CConstraint, CSMT, CLlvm, CCached :: CLContext
-pattern CInternalise = CLNullary CtxInternalise
-pattern CMatch = CLNullary CtxMatch
-pattern CDefinedness = CLNullary CtxDefinedness
-pattern CConstraint = CLNullary CtxConstraint
-pattern CSMT = CLNullary CtxSMT
-pattern CLlvm = CLNullary CtxLlvm
-pattern CCached = CLNullary CtxCached
-
--- results
-pattern CFailure, CIndeterminate, CAbort, CSuccess, CBreak, CContinue :: CLContext
-pattern CFailure = CLNullary CtxFailure
-pattern CIndeterminate = CLNullary CtxIndeterminate
-pattern CAbort = CLNullary CtxAbort
-pattern CSuccess = CLNullary CtxSuccess
-pattern CBreak = CLNullary CtxBreak
-pattern CContinue = CLNullary CtxContinue
-
--- information
-pattern CKoreTerm, CDetail, CSubstitution, CDepth :: CLContext
-pattern CKoreTerm = CLNullary CtxKoreTerm
-pattern CDetail = CLNullary CtxDetail
-pattern CSubstitution = CLNullary CtxSubstitution
-pattern CDepth = CLNullary CtxDepth
-
--- standard log levels
-pattern CError, CWarn, CInfo :: CLContext
-pattern CError = CLNullary CtxError
-pattern CWarn = CLNullary CtxWarn
-pattern CInfo = CLNullary CtxInfo
-
 -- translation table for nullary constructors
 translateSimple :: [(SimpleContext, String)]
 translateSimple =
@@ -171,17 +123,7 @@ instance Show IdContext where
     show (CtxFunction uid) = "function " <> show uid
     show (CtxCeil uid) = "ceil " <> show uid
     show (CtxTerm uid) = "term " <> show uid
-    show (CtxHook name) = "simplification " <> unpack name
-
-pattern CRewrite, CSimplification, CFunction, CCeil, CTerm :: UniqueId -> CLContext
-pattern CRewrite u = CLWithId (CtxRewrite u)
-pattern CSimplification u = CLWithId (CtxSimplification u)
-pattern CFunction u = CLWithId (CtxFunction u)
-pattern CCeil u = CLWithId (CtxCeil u)
-pattern CTerm u = CLWithId (CtxTerm u)
-
-pattern CHook :: Text -> CLContext
-pattern CHook t = CLWithId (CtxHook t)
+    show (CtxHook name) = "hook " <> unpack name
 
 ----------------------------------------
 data UniqueId

From bb299339eaa3ad24065d0ea121fa434ef9330679 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 19 Jun 2024 22:24:53 +1000
Subject: [PATCH 10/16] convert count-aborts app, make context a 'Seq' in
 LogLine

---
 dev-tools/count-aborts/Main.hs                | 37 ++++++++++++++++++-
 dev-tools/package.yaml                        |  1 +
 .../src/Kore/JsonRpc/Types/ContextLog.hs      |  3 +-
 3 files changed, 38 insertions(+), 3 deletions(-)

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/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/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index fc4b649f25..a460fe2ab4 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -13,6 +13,7 @@ import Data.List (stripPrefix)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
+import Data.Sequence (Seq)
 import Data.Text (Text, pack, unpack)
 import Data.Text qualified as Text
 import Data.Tuple (swap)
@@ -159,7 +160,7 @@ instance ToJSON UniqueId where
 
 ----------------------------------------
 data LogLine = LogLine
-    { context :: [CLContext]
+    { context :: Seq CLContext
     , message :: CLMessage
     }
     deriving stock (Generic, Show, Eq)

From a88045506daff8b988fff79f058a33ebead49750 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Thu, 20 Jun 2024 12:04:09 +1000
Subject: [PATCH 11/16] Use TH to derive the JSON instances (for performance)

---
 .../src/Kore/JsonRpc/Types/ContextLog.hs      | 120 ++++++++----------
 1 file changed, 50 insertions(+), 70 deletions(-)

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index a460fe2ab4..4443680aa6 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TemplateHaskell #-}
+
 {- |
 Copyright   : (c) Runtime Verification, 2023
 License     : BSD-3-Clause
@@ -6,54 +8,14 @@ module Kore.JsonRpc.Types.ContextLog (
     module Kore.JsonRpc.Types.ContextLog,
 ) where
 
-import Data.Aeson.Types (FromJSON (..), ToJSON (..))
+import Data.Aeson.TH (deriveJSON)
+import Data.Aeson.Types (FromJSON (..), Options (..), ToJSON (..), defaultOptions)
 import Data.Aeson.Types qualified as JSON
-import Data.Data
-import Data.List (stripPrefix)
-import Data.Map (Map)
-import Data.Map qualified as Map
-import Data.Maybe (fromMaybe)
+import Data.Char (toLower)
 import Data.Sequence (Seq)
-import Data.Text (Text, pack, unpack)
+import Data.Text (Text, unpack)
 import Data.Text qualified as Text
-import Data.Tuple (swap)
-import Deriving.Aeson
 
-data CLContext
-    = CLNullary SimpleContext
-    | CLWithId IdContext
-    deriving stock (Generic, Eq)
-
-instance Show CLContext where
-    show (CLNullary c) = fromMaybe (error $ show c) $ Map.lookup c simpleShow
-    show (CLWithId withId) = show withId
-
-instance ToJSON CLContext where
-    toJSON (CLNullary c) = JSON.String $ maybe (error $ show c) pack $ Map.lookup c simpleShow
-    toJSON (CLWithId withId) = JSON.genericToJSON options withId
-
-instance FromJSON CLContext where
-    parseJSON = \case
-        JSON.String simple
-            | Just c <- Map.lookup (unpack simple) simpleRead ->
-                pure $ CLNullary c
-        obj@JSON.Object{} ->
-            CLWithId <$> JSON.genericParseJSON options obj
-        other ->
-            JSON.typeMismatch "Object or string" other
-
-options :: JSON.Options
-options =
-    JSON.defaultOptions
-        { JSON.sumEncoding = JSON.ObjectWithSingleField
-        , JSON.constructorTagModifier = toJsonName
-        , JSON.allNullaryToStringTag = True
-        }
-
-toJsonName :: String -> String
-toJsonName name = JSON.camelTo2 '-' $ fromMaybe name $ stripPrefix "Ctx" name
-
-----------------------------------------
 data SimpleContext
     = -- component
       CtxBooster
@@ -89,20 +51,10 @@ data SimpleContext
       CtxError
     | CtxWarn
     | CtxInfo
-    deriving stock (Generic, Data, Enum, Show, Eq, Ord)
-
--- translation table for nullary constructors
-translateSimple :: [(SimpleContext, String)]
-translateSimple =
-    [ (con, toJsonName $ show con)
-    | con <- [CtxBooster .. CtxInfo]
-    ]
-
-simpleShow :: Map SimpleContext String
-simpleShow = Map.fromList translateSimple
+    deriving stock (Show, Eq, Ord, Enum)
 
-simpleRead :: Map String SimpleContext
-simpleRead = Map.fromList $ map swap translateSimple
+-- JSON encoding: strings dropping the 3-letter prefix and lower-case-ing
+$(deriveJSON defaultOptions{constructorTagModifier = map toLower . drop 3} ''SimpleContext)
 
 ----------------------------------------
 data IdContext
@@ -114,9 +66,7 @@ data IdContext
     | CtxTerm UniqueId
     | -- entities with name
       CtxHook Text
-    deriving stock (Generic, Eq)
-
--- To/FromJSON by way of Generic
+    deriving stock (Eq)
 
 instance Show IdContext where
     show (CtxRewrite uid) = "rewrite " <> show uid
@@ -131,7 +81,7 @@ data UniqueId
     = ShortId Text -- short hashes (7 char)
     | LongId Text -- long hashes (64 char)
     | UNKNOWN
-    deriving stock (Generic, Eq, Ord)
+    deriving stock (Eq, Ord)
 
 instance Show UniqueId where
     show (ShortId x) = unpack x
@@ -158,20 +108,42 @@ instance ToJSON UniqueId where
         LongId x -> JSON.String x
         UNKNOWN -> JSON.String "UNKNOWN"
 
+$( deriveJSON
+    defaultOptions
+        { JSON.constructorTagModifier = JSON.camelTo2 '-' . drop 3
+        , JSON.sumEncoding = JSON.ObjectWithSingleField
+        }
+    ''IdContext
+ )
+
 ----------------------------------------
-data LogLine = LogLine
-    { context :: Seq CLContext
-    , message :: CLMessage
-    }
-    deriving stock (Generic, Show, Eq)
-    deriving
-        (FromJSON, ToJSON)
-        via CustomJSON '[] LogLine
+data CLContext
+    = CLNullary SimpleContext
+    | CLWithId IdContext
+    deriving stock (Eq)
 
+instance Show CLContext where
+    show (CLNullary c) = map toLower . drop 3 $ 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 (Generic, Eq)
+    deriving stock (Eq)
 
 instance Show CLMessage where
     show (CLText t) = unpack t
@@ -188,3 +160,11 @@ instance FromJSON CLMessage where
 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)

From a510b1a56853157a2967578af526172f9586abe2 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Thu, 20 Jun 2024 14:14:11 +1000
Subject: [PATCH 12/16] fix kore-term tag (requires camelcase-ing)

---
 .../simplify-log.txt.golden                   | 30 -------------------
 .../src/Kore/JsonRpc/Types/ContextLog.hs      |  8 +++--
 2 files changed, 6 insertions(+), 32 deletions(-)

diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
index 0a8fee5466..9d0628ae6e 100644
--- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
+++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
@@ -5,72 +5,42 @@
 {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"}
 {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\")"}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"80d934c"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} \"$n\""}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"5875655"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"4a555cf"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f2fa0db"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"5a046bd"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f464178"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"5a046bd"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f464178"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"9893c04"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"5b84449"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(VarN:SortInt{}, \"0\")"}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=Int_(VarN:SortInt{}, \"0\"))"}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]]}}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k :  (24, 10)"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"8f1e2b8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}}}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
-{"context":["booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
 {"context":["kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
-{"context":["booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","simplify",{"term":"66aa67b"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]]}}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k :  (24, 10)"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"Eq#VarA","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"EVar","name":"Eq#VarB","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]]}}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k :  (23, 10)"}
 {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"success",{"term":"f6384ee"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}}}
-{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
-{"context":["booster","simplify",{"term":"931632b"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":["proxy"],"message":"Server shutting down"}
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 4443680aa6..12341f3879 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -53,8 +53,12 @@ data SimpleContext
     | CtxInfo
     deriving stock (Show, Eq, Ord, Enum)
 
--- JSON encoding: strings dropping the 3-letter prefix and lower-case-ing
-$(deriveJSON defaultOptions{constructorTagModifier = map toLower . drop 3} ''SimpleContext)
+$( deriveJSON
+    defaultOptions
+        { JSON.constructorTagModifier = JSON.camelTo2 '-' . drop 3
+        , JSON.sumEncoding = JSON.ObjectWithSingleField
+        }
+ ''SimpleContext)
 
 ----------------------------------------
 data IdContext

From bcef5c38224a480a1b38b59ab8c4f0b734651d31 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Thu, 20 Jun 2024 14:26:32 +1000
Subject: [PATCH 13/16] pimp show instance for SimpleContext to match json
 representation

---
 kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 12341f3879..ae3e45483b 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -9,9 +9,10 @@ module Kore.JsonRpc.Types.ContextLog (
 ) where
 
 import Data.Aeson.TH (deriveJSON)
-import Data.Aeson.Types (FromJSON (..), Options (..), ToJSON (..), defaultOptions)
+import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions)
 import Data.Aeson.Types qualified as JSON
 import Data.Char (toLower)
+import Data.Data (Data, toConstr)
 import Data.Sequence (Seq)
 import Data.Text (Text, unpack)
 import Data.Text qualified as Text
@@ -51,7 +52,10 @@ data SimpleContext
       CtxError
     | CtxWarn
     | CtxInfo
-    deriving stock (Show, Eq, Ord, Enum)
+    deriving stock (Eq, Ord, Enum, Data)
+
+instance Show SimpleContext where
+    show = JSON.camelTo2 '-' . drop 3 . show . toConstr
 
 $( deriveJSON
     defaultOptions
@@ -127,7 +131,7 @@ data CLContext
     deriving stock (Eq)
 
 instance Show CLContext where
-    show (CLNullary c) = map toLower . drop 3 $ show c
+    show (CLNullary c) = show c
     show (CLWithId withId) = show withId
 
 instance ToJSON CLContext where

From 3257cc5b573605d27b7265926f05d0fa1cd2efa7 Mon Sep 17 00:00:00 2001
From: github-actions <github-actions@github.com>
Date: Thu, 20 Jun 2024 05:35:53 +0000
Subject: [PATCH 14/16] Format with fourmolu

---
 kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index ae3e45483b..0ba4942c25 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -62,7 +62,8 @@ $( deriveJSON
         { JSON.constructorTagModifier = JSON.camelTo2 '-' . drop 3
         , JSON.sumEncoding = JSON.ObjectWithSingleField
         }
- ''SimpleContext)
+    ''SimpleContext
+ )
 
 ----------------------------------------
 data IdContext

From 0138c9976eff2c1fcd676416e290961946a1eef6 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Thu, 20 Jun 2024 15:37:30 +1000
Subject: [PATCH 15/16] remove redundant import

---
 kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 0ba4942c25..dc87190377 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -11,7 +11,6 @@ module Kore.JsonRpc.Types.ContextLog (
 import Data.Aeson.TH (deriveJSON)
 import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions)
 import Data.Aeson.Types qualified as JSON
-import Data.Char (toLower)
 import Data.Data (Data, toConstr)
 import Data.Sequence (Seq)
 import Data.Text (Text, unpack)

From 8c334344c2e05f975405c7bfc3bde969ee11ddc4 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Thu, 20 Jun 2024 17:01:01 +1000
Subject: [PATCH 16/16] Anti-capitalism

---
 booster/library/Booster/SMT/Interface.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs
index 12137371ca..5d0fd5b0c1 100644
--- a/booster/library/Booster/SMT/Interface.hs
+++ b/booster/library/Booster/SMT/Interface.hs
@@ -169,7 +169,7 @@ getModelFor ::
     io (Either SMTError (Either SMT.Response (Map Variable Term)))
 getModelFor ctxt ps subst
     | null ps && Map.null subst = Log.withContext Log.CtxSMT $ do
-        Log.logMessage ("No Constraints Or Substitutions To Check, Returning Sat" :: Text)
+        Log.logMessage ("No constraints or substitutions to check, returning Sat" :: Text)
         pure . Right . Right $ Map.empty
     | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do
         Log.logMessage $ "SMT translation error: " <> errMsg