Add Fallback to LogEntry (#3657)

This PR modifies the `LogEntry` type in `kore-rpc-types` in two ways:
* add `origianlTerm` into `Rewrite` log entry constructor (and emit
Nothing for now in Kore to retain the current behavior. This change is
not necessary at the moment, but we may need to log these terms in
future.
* Add `Fallback` constructor to `LogEntry` to enable `kore-rpc-booster`
to emit a trace when it falls back from Booster to Kore.

kore-rpc-types/kore-rpc-types.cabal

@@ -84,6 +84,7 @@ library
     Kore.JsonRpc.Error
     Kore.JsonRpc.Types
     Kore.JsonRpc.Types.Log
+    Kore.JsonRpc.Types.Depth
     Kore.JsonRpc.Server
     Kore.Syntax.Json.Types
   hs-source-dirs:

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

@@ -4,6 +4,7 @@ License     : BSD-3-Clause
 -}
 module Kore.JsonRpc.Types (
     module Kore.JsonRpc.Types,
+    module Kore.JsonRpc.Types.Depth,
 ) where
 
 import Control.Exception (Exception)
@@ -19,18 +20,14 @@ import Deriving.Aeson (
     StripPrefix,
  )
 import GHC.Generics (Generic)
+import Kore.JsonRpc.Types.Depth (Depth (..))
 import Kore.JsonRpc.Types.Log (LogEntry)
 import Kore.Syntax.Json.Types (KoreJson)
 import Network.JSONRPC (
     FromRequest (..),
  )
-import Numeric.Natural
 import Prettyprinter qualified as Pretty
 
-newtype Depth = Depth {getNat :: Natural}
-    deriving stock (Show, Eq)
-    deriving newtype (FromJSON, ToJSON, Num)
-
 data ExecuteRequest = ExecuteRequest
     { state :: !KoreJson
     , maxDepth :: !(Maybe Depth)
@@ -43,6 +40,7 @@ data ExecuteRequest = ExecuteRequest
     , logFailedRewrites :: !(Maybe Bool)
     , logSuccessfulSimplifications :: !(Maybe Bool)
     , logFailedSimplifications :: !(Maybe Bool)
+    , logFallbacks :: !(Maybe Bool)
     }
     deriving stock (Generic, Show, Eq)
     deriving

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

@@ -0,0 +1,8 @@
+module Kore.JsonRpc.Types.Depth (module Kore.JsonRpc.Types.Depth) where
+
+import Data.Aeson.Types (FromJSON (..), ToJSON (..))
+import Numeric.Natural
+
+newtype Depth = Depth {getNat :: Natural}
+    deriving stock (Show, Eq)
+    deriving newtype (FromJSON, ToJSON, Num)

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

@@ -3,8 +3,10 @@
 module Kore.JsonRpc.Types.Log (module Kore.JsonRpc.Types.Log) where
 
 import Data.Aeson (FromJSON, ToJSON)
+import Data.List.NonEmpty (NonEmpty)
 import Data.Text (Text)
 import GHC.Generics (Generic)
+import Kore.JsonRpc.Types.Depth (Depth (..))
 import Kore.Syntax.Json.Types (KoreJson)
 
 import Deriving.Aeson (
@@ -16,7 +18,7 @@ import Deriving.Aeson (
     StripPrefix,
  )
 
-data LogOrigin = KoreRpc | Booster | Llvm
+data LogOrigin = KoreRpc | Booster | Llvm | Proxy
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)
@@ -26,13 +28,13 @@ data LogOrigin = KoreRpc | Booster | Llvm
 
 data LogRewriteResult
     = Success
-        { rewrittenTerm :: Maybe KoreJson
-        , substitution :: Maybe KoreJson
-        , ruleId :: Text
+        { rewrittenTerm :: !(Maybe KoreJson)
+        , substitution :: !(Maybe KoreJson)
+        , ruleId :: !Text
         }
     | Failure
-        { reason :: Text
-        , _ruleId :: Maybe Text
+        { reason :: !Text
+        , _ruleId :: !(Maybe Text)
         }
     deriving stock (Generic, Show, Eq)
     deriving
@@ -46,14 +48,31 @@ data LogRewriteResult
 
 data LogEntry
     = Rewrite
-        { result :: LogRewriteResult
-        , origin :: LogOrigin
+        { result :: !(LogRewriteResult)
+        , origin :: !LogOrigin
         }
     | Simplification
-        { originalTerm :: Maybe KoreJson
-        , originalTermIndex :: Maybe [Int]
-        , result :: LogRewriteResult
-        , origin :: LogOrigin
+        { originalTerm :: !(Maybe KoreJson)
+        , originalTermIndex :: !(Maybe [Int])
+        , result :: !LogRewriteResult
+        , origin :: !LogOrigin
+        }
+    | -- | Indicates a fallback of an RPC-server to a more powerful, but slower backup server, i.e. Booster to Kore
+      Fallback
+        { originalTerm :: !(Maybe KoreJson)
+        -- ^ state before fallback
+        , rewrittenTerm :: !(Maybe KoreJson)
+        -- ^ state after fallback
+        , reason :: !Text
+        -- ^ fallback reason
+        , fallbackRuleId :: !Text
+        -- ^ the rule that caused the fallback
+        , recoveryRuleIds :: !(Maybe (NonEmpty Text))
+        -- ^ rules applied during fallback, the first rule is the one that caused the fallback
+        , recoveryDepth :: !Depth
+        -- ^ depth reached in fallback, must be the same as (length ruleIds)
+        , origin :: !LogOrigin
+        -- ^ proxy server the log was emitted from
         }
     deriving stock (Generic, Show, Eq)
     deriving