Add Fallback to LogEntry

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