RPC trace cleanup: remove simplification logs (#3880)

Fixes #3871

Note that removing the simplification log request parameters and the
simplification log entries form the response is same, because `pyk` is
already modified to not recognize them, see:

- the `LogEntry`
[type](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L543)
- the parameters for
[execute](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L1003),
[simplify](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L1049)
and
[implies](https://github.com/runtimeverification/k/blob/develop/pyk/src/pyk/kore/rpc.py#L1030)
request

But even considering that, we should run `pyk`'s integration tests
before merging.

booster/library/Booster/Definition/Ceil.hs

@@ -101,7 +101,7 @@ computeCeilRule ::
 computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
     | null computedAttributes.notPreservesDefinednessReasons = pure Nothing
     | otherwise = do
-        (res, _) <- runEquationT (Flag False) def mllvm Nothing mempty $ do
+        (res, _) <- runEquationT def mllvm Nothing mempty $ do
             lhsCeils <- Set.fromList <$> computeCeil lhs
             requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
             let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -15,10 +15,6 @@ module Booster.Pattern.ApplyEquations (
     getConfig,
     EquationPreference (..),
     EquationFailure (..),
-    EquationTrace (..),
-    pattern CollectEquationTraces,
-    pattern NoCollectEquationTraces,
-    eraseStates,
     EquationMetadata (..),
     ApplyEquationResult (..),
     ApplyEquationFailure (..),
@@ -85,7 +81,7 @@ import Booster.Pattern.Util
 import Booster.Prettyprinter (renderDefault, renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
-import Booster.Util (Bound (..), Flag (..))
+import Booster.Util (Bound (..))
 import Kore.JsonRpc.Types.Log qualified as KoreRpcLog
 import Kore.Util (showHashHex)
 
@@ -152,18 +148,11 @@ data EquationConfig = EquationConfig
     { definition :: KoreDefinition
     , llvmApi :: Maybe LLVM.API
     , smtSolver :: Maybe SMT.SMTContext
-    , doTracing :: Flag "CollectEquationTraces"
     , maxRecursion :: Bound "Recursion"
     , maxIterations :: Bound "Iterations"
     , logger :: Logger LogMessage
     }
 
-pattern CollectEquationTraces :: Flag "CollectEquationTraces"
-pattern CollectEquationTraces = Flag True
-
-pattern NoCollectEquationTraces :: Flag "CollectEquationTraces"
-pattern NoCollectEquationTraces = Flag False
-
 data EquationState = EquationState
     { termStack :: Seq Term
     , recursionStack :: [Term]
@@ -197,15 +186,6 @@ data EquationTrace term
     | EquationNotApplied term EquationMetadata ApplyEquationFailure
     deriving stock (Eq, Show)
 
-{- | For the given equation trace, construct a new one,
-     removing the heavy-weight information (the states),
-     but keeping the meta-data (rule labels).
--}
-eraseStates :: EquationTrace Term -> EquationTrace ()
-eraseStates = \case
-    EquationApplied _ metadata _ -> EquationApplied () metadata ()
-    EquationNotApplied _ metadata failureInfo -> EquationNotApplied () metadata failureInfo
-
 instance Pretty (EquationTrace Term) where
     pretty (EquationApplied subjectTerm metadata rewritten) =
         vsep
@@ -415,14 +395,13 @@ data EquationPreference = PreferFunctions | PreferSimplifications
 
 runEquationT ::
     LoggerMIO io =>
-    Flag "CollectEquationTraces" ->
     KoreDefinition ->
     Maybe LLVM.API ->
     Maybe SMT.SMTContext ->
     SimplifierCache ->
     EquationT io a ->
     io (Either EquationFailure a, SimplifierCache)
-runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do
+runEquationT definition llvmApi smtSolver sCache (EquationT m) = do
     globalEquationOptions <- liftIO GlobalState.readGlobalEquationOptions
     logger <- getLogger
     (res, endState) <-
@@ -434,7 +413,6 @@ runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do
                         { definition
                         , llvmApi
                         , smtSolver
-                        , doTracing
                         , maxIterations = globalEquationOptions.maxIterations
                         , maxRecursion = globalEquationOptions.maxRecursion
                         , logger
@@ -537,15 +515,14 @@ llvmSimplify term = do
 evaluateTerm ::
     LoggerMIO io =>
     MonadLoggerIO io =>
-    Flag "CollectEquationTraces" ->
     Direction ->
     KoreDefinition ->
     Maybe LLVM.API ->
     Maybe SMT.SMTContext ->
     Term ->
     io (Either EquationFailure Term, SimplifierCache)
-evaluateTerm doTracing direction def llvmApi smtSolver =
-    runEquationT doTracing def llvmApi smtSolver mempty
+evaluateTerm direction def llvmApi smtSolver =
+    runEquationT def llvmApi smtSolver mempty
         . evaluateTerm' direction
 
 -- version for internal nested evaluation
@@ -562,15 +539,14 @@ evaluateTerm' direction = iterateEquations direction PreferFunctions
 evaluatePattern ::
     LoggerMIO io =>
     MonadLoggerIO io =>
-    Flag "CollectEquationTraces" ->
     KoreDefinition ->
     Maybe LLVM.API ->
     Maybe SMT.SMTContext ->
     SimplifierCache ->
     Pattern ->
     io (Either EquationFailure Pattern, SimplifierCache)
-evaluatePattern doTracing def mLlvmLibrary smtSolver cache =
-    runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluatePattern'
+evaluatePattern def mLlvmLibrary smtSolver cache =
+    runEquationT def mLlvmLibrary smtSolver cache . evaluatePattern'
 
 -- version for internal nested evaluation
 evaluatePattern' ::
@@ -600,15 +576,14 @@ simplifyAssumedPredicate p = do
 evaluateConstraints ::
     LoggerMIO io =>
     MonadLoggerIO io =>
-    Flag "CollectEquationTraces" ->
     KoreDefinition ->
     Maybe LLVM.API ->
     Maybe SMT.SMTContext ->
     SimplifierCache ->
     Set Predicate ->
     io (Either EquationFailure (Set Predicate), SimplifierCache)
-evaluateConstraints doTracing def mLlvmLibrary smtSolver cache =
-    runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluateConstraints'
+evaluateConstraints def mLlvmLibrary smtSolver cache =
+    runEquationT def mLlvmLibrary smtSolver cache . evaluateConstraints'
 
 evaluateConstraints' ::
     LoggerMIO io =>
@@ -1084,28 +1059,26 @@ applyEquation term rule = withRuleContext rule $ fmap (either Failure Success) $
 simplifyConstraint ::
     LoggerMIO io =>
     MonadLoggerIO io =>
-    Flag "CollectEquationTraces" ->
     KoreDefinition ->
     Maybe LLVM.API ->
     Maybe SMT.SMTContext ->
     SimplifierCache ->
     Predicate ->
     io (Either EquationFailure Predicate, SimplifierCache)
-simplifyConstraint doTracing def mbApi mbSMT cache (Predicate p) = do
-    runEquationT doTracing def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p
+simplifyConstraint def mbApi mbSMT cache (Predicate p) = do
+    runEquationT def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p
 
 simplifyConstraints ::
     LoggerMIO io =>
     MonadLoggerIO io =>
-    Flag "CollectEquationTraces" ->
     KoreDefinition ->
     Maybe LLVM.API ->
     Maybe SMT.SMTContext ->
     SimplifierCache ->
     [Predicate] ->
     io (Either EquationFailure [Predicate], SimplifierCache)
-simplifyConstraints doTracing def mbApi mbSMT cache ps =
-    runEquationT doTracing def mbApi mbSMT cache $
+simplifyConstraints def mbApi mbSMT cache ps =
+    runEquationT def mbApi mbSMT cache $
         concatMap splitAndBools
             <$> mapM ((coerce <$>) . simplifyConstraint' True . coerce) ps
 

booster/library/Booster/Pattern/Rewrite.hs

@@ -57,12 +57,10 @@ import Booster.Log (
  )
 import Booster.Pattern.ApplyEquations (
     EquationFailure (..),
-    EquationTrace,
     SimplifierCache,
     evaluatePattern,
     simplifyConstraint,
  )
-import Booster.Pattern.ApplyEquations qualified as ApplyEquations
 import Booster.Pattern.Base
 import Booster.Pattern.Bool
 import Booster.Pattern.Index (TermIndex (..), kCellTermIndex)
@@ -97,9 +95,6 @@ instance MonadLoggerIO io => LoggerMIO (RewriteT io) where
     getLogger = RewriteT $ asks logger
     withLogger modL (RewriteT m) = RewriteT $ withReaderT (\cfg@RewriteConfig{logger} -> cfg{logger = modL logger}) m
 
-castDoTracingFlag :: Flag "CollectRewriteTraces" -> Flag "CollectEquationTraces"
-castDoTracingFlag = coerce
-
 pattern CollectRewriteTraces :: Flag "CollectRewriteTraces"
 pattern CollectRewriteTraces = Flag True
 
@@ -439,11 +434,11 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
         Predicate ->
         RewriteRuleAppT (RewriteT io) (Maybe a)
     checkConstraint onUnclear onBottom p = do
-        RewriteConfig{definition, llvmApi, smtSolver, doTracing} <- lift $ RewriteT ask
+        RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask
         oldCache <- lift . RewriteT . lift $ get
         (simplified, cache) <-
             withContext "constraint" $
-                simplifyConstraint (castDoTracingFlag doTracing) definition llvmApi smtSolver oldCache p
+                simplifyConstraint definition llvmApi smtSolver oldCache p
         -- update cache
         lift . RewriteT . lift . modify $ const cache
         -- TODO should we keep the traces? Or only on success?
@@ -547,11 +542,7 @@ data RewriteTrace pat
     | -- | attempted rewrite failed
       RewriteStepFailed (RewriteFailed "Rewrite")
     | -- | Applied simplification to the pattern
-      RewriteSimplified [EquationTrace (TracePayload pat)] (Maybe EquationFailure)
-
-type family TracePayload pat where
-    TracePayload Pattern = Term
-    TracePayload () = ()
+      RewriteSimplified (Maybe EquationFailure)
 
 {- | For the given rewrite trace, construct a new one,
      removing the heavy-weight information (the states),
@@ -562,8 +553,7 @@ eraseStates = \case
     RewriteSingleStep rule_label mUniqueId _preState _postState -> RewriteSingleStep rule_label mUniqueId () ()
     RewriteBranchingStep _state branchMetadata -> RewriteBranchingStep () branchMetadata
     RewriteStepFailed failureInfo -> RewriteStepFailed failureInfo
-    RewriteSimplified equationTraces mbEquationFailure ->
-        RewriteSimplified (map ApplyEquations.eraseStates equationTraces) mbEquationFailure
+    RewriteSimplified mbEquationFailure -> RewriteSimplified mbEquationFailure
 
 instance Pretty (RewriteTrace Pattern) where
     pretty = \case
@@ -741,25 +731,25 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
         st <- get
         let cache = st.simplifierCache
             smt = st.smtSolver
-        evaluatePattern (castDoTracingFlag doTracing) def mLlvmLibrary smt cache p >>= \(res, newCache) -> do
+        evaluatePattern def mLlvmLibrary smt cache p >>= \(res, newCache) -> do
             updateCache newCache
             case res of
                 Right newPattern -> do
-                    emitRewriteTrace $ RewriteSimplified [] Nothing
+                    emitRewriteTrace $ RewriteSimplified Nothing
                     pure $ Just newPattern
                 Left r@(SideConditionFalse _p) -> do
                     logSimplify "A side condition was found to be false, pruning"
-                    emitRewriteTrace $ RewriteSimplified [] (Just r)
+                    emitRewriteTrace $ RewriteSimplified (Just r)
                     pure Nothing
                 Left r@UndefinedTerm{} -> do
                     logSimplify "Term is undefined, pruning"
-                    emitRewriteTrace $ RewriteSimplified [] (Just r)
+                    emitRewriteTrace $ RewriteSimplified (Just r)
                     pure Nothing
                 Left r@(TooManyIterations n _start _result) -> do
                     logSimplify $
                         "Unable to simplify in " <> Text.pack (show n) <> " iterations, returning original"
                     -- warning has been printed inside ApplyEquation.evaluatePattern
-                    emitRewriteTrace $ RewriteSimplified [] (Just r)
+                    emitRewriteTrace $ RewriteSimplified (Just r)
                     -- NB start/result in this error are terms and might come
                     -- from simplifying one of the constraints. Therefore, the
                     -- original pattern must be returned.
@@ -773,11 +763,11 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
                                 <> prettyText l
                                 <> ": \n"
                                 <> Text.unlines (map (prettyText . fst) termDiffs)
-                    emitRewriteTrace $ RewriteSimplified [] (Just r)
+                    emitRewriteTrace $ RewriteSimplified (Just r)
                     pure $ Just p
                 Left other -> do
                     logError $ "Simplification error during rewrite: " <> (Text.pack . constructorName $ other)
-                    emitRewriteTrace $ RewriteSimplified [] (Just other)
+                    emitRewriteTrace $ RewriteSimplified (Just other)
                     pure $ Just p
 
     -- Results may change when simplification prunes a false side

booster/tools/booster/Proxy.hs

@@ -90,9 +90,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
         | otherwise ->
             let logSettings =
                     LogSettings
-                        { logSuccessfulSimplifications = execReq.logSuccessfulSimplifications
-                        , logFailedSimplifications = execReq.logFailedSimplifications
-                        , logSuccessfulRewrites = execReq.logSuccessfulRewrites
+                        { logSuccessfulRewrites = execReq.logSuccessfulRewrites
                         , logFailedRewrites = execReq.logFailedRewrites
                         , logFallbacks = execReq.logFallbacks
                         , logTiming = execReq.logTiming
@@ -550,8 +548,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                 SimplifyRequest
                     { state = execStateToKoreJson state
                     , _module = mbModule
-                    , logSuccessfulSimplifications = Nothing
-                    , logFailedSimplifications = Nothing
                     , logTiming
                     }
 
@@ -612,9 +608,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                     }
 
 data LogSettings = LogSettings
-    { logSuccessfulSimplifications :: Maybe Bool
-    , logFailedSimplifications :: Maybe Bool
-    , logSuccessfulRewrites :: Maybe Bool
+    { logSuccessfulRewrites :: Maybe Bool
     , logFailedRewrites :: Maybe Bool
     , logFallbacks :: Maybe Bool
     , logTiming :: Maybe Bool

booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs

@@ -98,7 +98,7 @@ test_evaluateFunction =
         unsafePerformIO
             . runNoLoggingT
             . (fst <$>)
-            . evaluateTerm NoCollectEquationTraces direction funDef Nothing Nothing
+            . evaluateTerm direction funDef Nothing Nothing
 
     isTooManyIterations (Left (TooManyIterations _n _ _)) = pure ()
     isTooManyIterations (Left err) = assertFailure $ "Unexpected error " <> show err
@@ -129,7 +129,7 @@ test_simplify =
         unsafePerformIO
             . runNoLoggingT
             . (fst <$>)
-            . evaluateTerm NoCollectEquationTraces direction simplDef Nothing Nothing
+            . evaluateTerm direction simplDef Nothing Nothing
     a = var "A" someSort
 
 test_simplifyPattern :: TestTree
@@ -159,7 +159,7 @@ test_simplifyPattern =
         unsafePerformIO
             . runNoLoggingT
             . (fst <$>)
-            . evaluatePattern NoCollectEquationTraces simplDef Nothing Nothing mempty
+            . evaluatePattern simplDef Nothing Nothing mempty
     a = var "A" someSort
 
 test_simplifyConstraint :: TestTree
@@ -229,7 +229,7 @@ test_simplifyConstraint =
         unsafePerformIO
             . runNoLoggingT
             . (fst <$>)
-            . simplifyConstraint NoCollectEquationTraces testDefinition Nothing Nothing mempty
+            . simplifyConstraint testDefinition Nothing Nothing mempty
 
 test_errors :: TestTree
 test_errors =
@@ -242,7 +242,7 @@ test_errors =
                 loopTerms =
                     [f $ app con1 [a], f $ app con2 [a], f $ app con3 [a, a], f $ app con1 [a]]
             isLoop loopTerms . unsafePerformIO . runNoLoggingT $
-                fst <$> evaluateTerm NoCollectEquationTraces TopDown loopDef Nothing Nothing subj
+                fst <$> evaluateTerm TopDown loopDef Nothing Nothing subj
         ]
   where
     isLoop ts (Left (EquationLoop ts')) = ts @?= ts'

kore-rpc-types/src/Kore/JsonRpc/Types.hs

@@ -39,8 +39,6 @@ data ExecuteRequest = ExecuteRequest
     , assumeStateDefined :: !(Maybe Bool)
     , logSuccessfulRewrites :: !(Maybe Bool)
     , logFailedRewrites :: !(Maybe Bool)
-    , logSuccessfulSimplifications :: !(Maybe Bool)
-    , logFailedSimplifications :: !(Maybe Bool)
     , logFallbacks :: !(Maybe Bool)
     , logTiming :: !(Maybe Bool)
     }
@@ -54,8 +52,6 @@ data ImpliesRequest = ImpliesRequest
     , consequent :: !KoreJson
     , _module :: !(Maybe Text)
     , assumeDefined :: !(Maybe Bool)
-    , logSuccessfulSimplifications :: !(Maybe Bool)
-    , logFailedSimplifications :: !(Maybe Bool)
     , logTiming :: !(Maybe Bool)
     }
     deriving stock (Generic, Show, Eq)
@@ -66,8 +62,6 @@ data ImpliesRequest = ImpliesRequest
 data SimplifyRequest = SimplifyRequest
     { state :: KoreJson
     , _module :: !(Maybe Text)
-    , logSuccessfulSimplifications :: !(Maybe Bool)
-    , logFailedSimplifications :: !(Maybe Bool)
     , logTiming :: !(Maybe Bool)
     }
     deriving stock (Generic, Show, Eq)