From 85b5d086840a0f1e89499f086b50d7258598fc8b Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Mon, 18 Sep 2023 10:33:19 +0200
Subject: [PATCH] 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           |  1 +
 kore-rpc-types/src/Kore/JsonRpc/Types.hs      |  8 ++--
 .../src/Kore/JsonRpc/Types/Depth.hs           |  8 ++++
 kore-rpc-types/src/Kore/JsonRpc/Types/Log.hs  | 43 +++++++++++++------
 4 files changed, 43 insertions(+), 17 deletions(-)
 create mode 100644 kore-rpc-types/src/Kore/JsonRpc/Types/Depth.hs

diff --git a/kore-rpc-types/kore-rpc-types.cabal b/kore-rpc-types/kore-rpc-types.cabal
index b5e0b776f2..c23055ed01 100644
--- a/kore-rpc-types/kore-rpc-types.cabal
+++ b/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:
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
index e39f9ad676..1d8f262ba5 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs
+++ b/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
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/Depth.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/Depth.hs
new file mode 100644
index 0000000000..4a239e958f
--- /dev/null
+++ b/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)
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/Log.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/Log.hs
index 9660b4bd68..5218a9fa23 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/Log.hs
+++ b/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