Types specifying the simplify-implication RPC endpoint

docs/2022-07-18-JSON-RPC-Server-API.md

@@ -388,6 +388,127 @@ Same as for execute
 }
 ```
 
+## Simplify Implication
+
+### Request:
+
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "method": "simplify-implication",
+  "params": {
+    "antecedent": {"format": "KORE", "version": 1, "term": {}},
+    "consequent": {"format": "KORE", "version": 1, "term": {}},
+    "module": "MODULE-NAME"
+  }
+}
+```
+
+Optional parameters: `module` (main module name)
+
+The request format is shared with the `"implies"` method.
+
+**NOTE**: `"simplify-implication"` currently only has a stub implementation in `kore-rpc`. The real implementation is in `kore-rpc-booster` (see [hs-backend-booster](https://github.com/runtimeverification/hs-backend-booster) repository). The documentation will reside here for consistency.
+
+### Error Response:
+
+Errors in decoding the `antecedent` or `consequent` terms are reported similar as for execute.
+
+### Correct Response:
+
+The endpoint is a lightweight variant fo the `"implies"` endpoint, which checks implication using matching between configuration terms and a lightweight (using K simplifications, rather than encoding to SMT) constraint subsumption.
+
+The implication can be "valid", "invalid" and "unknown". The result is returned in the `"validity"` field. The following results are possible:
+
+#### Implication is **valid**
+
+A constrained substitution as the result, and this is only returned if the implication is valid.
+
+```
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "result": {
+    "validity": {"tag": "implication-valid"},
+    "substitution": {"format": "KORE", "version": 1, "term": {}},
+  }
+}
+```
+
+#### Implication **invalid**: terms do not match
+
+Matching between antecedent and consequent configurations failed (different constructors, shared variables, sort error, etc.), constraints has not been subsumption been attempted. No matching substitution is returned.
+
+```
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "result": {
+    "validity": {"tag": "implication-valid",
+                 "contents": {"tag": "matching-failed",
+                              "contents": "Shared variables: X:SortWordStack{}"
+                 }},
+  }
+}
+```
+
+#### Implication **invalid**: terms match, but constraints subsumption failed
+
+Matching between antecedent and consequent configurations is successful, but constraints do not agree. Response contains the matching substitution and the unsatisfiable core of constraints.
+
+```
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "result": {
+    "validity": {"tag": "implication-valid",
+                 "contents": {"tag": "constraint-subsumption-failed",
+                              "contents": {"format": "KORE", "version": 1, "term": {}}
+                 }},
+    "substitution": {"format": "KORE", "version": 1, "term": {}},
+  }
+}
+```
+
+#### Implication **unknown**: matching indeterminate
+
+The matching algorithm is incomplete and may return an indeterminate result. The response will contains the subterms that the algorithm could not know how to match. No substitution is returned.
+
+```
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "result": {
+    "validity": {"tag": "implication-unknown",
+                 "contents": {"tag": "matching-unknown",
+                              "contents": {"first" : {"format": "KORE", "version": 1, "term": {}}
+                                          ,"second" : {"format": "KORE", "version": 1, "term": {}}
+                                          }
+                 }},
+  }
+}
+```
+
+#### Implication **unknown**: constraint subsumption indeterminate
+
+If matching is successful, but the constraint solver procedure (internal, or the SMT solver if enabled) returned "unknown". Response contains the matching substitution and the unknown core of constraints.
+
+```
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "result": {
+    "validity": {"tag": "implication-unknown",
+                 "contents": {"tag": "constraint-subsumption-unknown",
+                              "contents": {"tag": "constraint-subsumption-failed",
+                                           "contents": {"format": "KORE", "version": 1, "term": {}}
+                 }},
+    "substitution": {"format": "KORE", "version": 1, "term": {}},
+  }
+}
+```
+
 ## Add-module
 
 ### Request

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

@@ -99,6 +99,7 @@ instance FromRequest (API 'Req) where
     parseParams "simplify" = Just $ fmap (Simplify <$>) parseJSON
     parseParams "add-module" = Just $ fmap (AddModule <$>) parseJSON
     parseParams "get-model" = Just $ fmap (GetModel <$>) parseJSON
+    parseParams "simplify-implication" = Just $ fmap (SimplifyImplication <$>) parseJSON
     parseParams "cancel" = Just $ const $ return Cancel
     parseParams _ = Nothing
 
@@ -177,6 +178,48 @@ data GetModelResult = GetModelResult
         (FromJSON, ToJSON)
         via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] GetModelResult
 
+data SimplifyImplicationResult = SimplifyImplicationResult
+    { validity :: ImplicationValidityResult
+    , substitution :: Maybe KoreJson
+    , logs :: Maybe [LogEntry]
+    }
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImplicationResult
+
+data ImplicationValidityResult
+    = -- | implication is valid
+      ImplicationValid
+    | -- | implication is invalid, explains why
+      ImplicationInvalid ImplicationInvalidReason
+    | -- | implication is unknown, explains why
+      ImplicationUnknown ImplicationUnknownReason
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[ConstructorTagModifier '[CamelToKebab]] ImplicationValidityResult
+
+data ImplicationInvalidReason
+    = -- | antecedent and consequent do not match
+      MatchingFailed Text
+    | -- | matching was successful, but constraints don't agree: return unsatisfiable core of constraints
+      ConstraintSubsumptionFailed KoreJson
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[ConstructorTagModifier '[CamelToKebab]] ImplicationInvalidReason
+
+data ImplicationUnknownReason
+    = -- | matching between antecedent and consequent is indeterminate, return the subterms that caused this
+      MatchingUnknown KoreJson KoreJson
+    | -- | matching was successful, but constraint subsumption is indeterminate: return unknown constraints
+      ConstraintSubsumptionUnknown KoreJson
+    deriving stock (Generic, Show, Eq)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[ConstructorTagModifier '[CamelToKebab]] ImplicationUnknownReason
+
 data SatResult
     = Sat
     | Unsat
@@ -194,6 +237,7 @@ data APIMethod
     | SimplifyM
     | AddModuleM
     | GetModelM
+    | SimplifyImplicationM
     deriving stock (Eq, Ord, Show, Enum)
 
 type family APIPayload (api :: APIMethod) (r :: ReqOrRes) where
@@ -207,13 +251,16 @@ type family APIPayload (api :: APIMethod) (r :: ReqOrRes) where
     APIPayload 'AddModuleM 'Res = ()
     APIPayload 'GetModelM 'Req = GetModelRequest
     APIPayload 'GetModelM 'Res = GetModelResult
+    APIPayload 'SimplifyImplicationM 'Req = ImpliesRequest
+    APIPayload 'SimplifyImplicationM 'Res = SimplifyImplicationResult
 
 data API (r :: ReqOrRes) where
     Execute :: APIPayload 'ExecuteM r -> API r
     Implies :: APIPayload 'ImpliesM r -> API r
     Simplify :: APIPayload 'SimplifyM r -> API r
     AddModule :: APIPayload 'AddModuleM r -> API r
     GetModel :: APIPayload 'GetModelM r -> API r
+    SimplifyImplication :: APIPayload 'SimplifyImplicationM r -> API r
     Cancel :: API 'Req
 
 deriving stock instance Show (API 'Req)
@@ -228,6 +275,7 @@ instance ToJSON (API 'Res) where
         Simplify payload -> toJSON payload
         AddModule payload -> toJSON payload
         GetModel payload -> toJSON payload
+        SimplifyImplication payload -> toJSON payload
 
 instance Pretty.Pretty (API 'Req) where
     pretty = \case
@@ -236,6 +284,7 @@ instance Pretty.Pretty (API 'Req) where
         Simplify _ -> "simplify"
         AddModule _ -> "add-module"
         GetModel _ -> "get-model"
+        SimplifyImplication _ -> "simplify-implication"
         Cancel -> "cancel"
 
 rpcJsonConfig :: PrettyJson.Config

kore/src/Kore/JsonRpc.hs

@@ -494,7 +494,13 @@ respond serverState moduleName runSMT =
                                             PatternJson.fromSubstitution sort $
                                                 Substitution.mapVariables getRewritingVariable subst
                                         }
-
+        SimplifyImplication ImpliesRequest{antecedent, consequent} ->
+            pure . Right . SimplifyImplication $
+                SimplifyImplicationResult
+                    { validity = ImplicationUnknown (MatchingUnknown antecedent consequent)
+                    , substitution = Nothing
+                    , logs = mempty
+                    }
         -- this case is only reachable if the cancel appeared as part of a batch request
         Cancel -> pure $ Left cancelUnsupportedInBatchMode
   where

test/rpc-server/runTests.py

@@ -254,3 +254,21 @@ def runTest(def_path, req, resp_golden_path):
       params["state"] = state
       req = rpc_request_id1("get-model", params)
       runTest(get_model_def_path, req, resp_golden_path)
+
+print("Running simplify-implication tests:")
+
+for name in os.listdir("./simplify-implication"):
+  info(f"- test '{name}'...")
+  simplify_implication_def_path = os.path.join("./simplify-implication", name, "definition.kore")
+  params_json_path = os.path.join("./simplify-implication", name, "antecedent.json")
+  state_json_path = os.path.join("./simplify-implication", name, "consequent.json")
+  resp_golden_path = os.path.join("./simplify-implication", name, "response.golden")
+  with open(params_json_path, 'r') as antecedent_json:
+    with open(state_json_path, 'r') as consequent_json:
+      antecedent = json.loads(antecedent_json.read())
+      consequent = json.loads(consequent_json.read())
+      params = {}
+      params["antecedent"] = antecedent
+      params["consequent"] = consequent
+      req = rpc_request_id1("simplify-implication", params)
+      runTest(simplify_implication_def_path, req, resp_golden_path)

test/rpc-server/simplify-implication/trivial-unknown/README.md

@@ -0,0 +1 @@
+`X => X`, response `ImplicationUnknown`, with empty substitution. `simplify-implication` is only implemented as a stub in `kore-rpc`.

test/rpc-server/simplify-implication/trivial-unknown/antecedent.json

@@ -0,0 +1,12 @@
+{
+    "format": "KORE",
+    "version": 1,
+    "term": {
+        "tag": "EVar",
+        "name": "X",
+        "sort": {
+            "tag": "SortVar",
+            "name": "S"
+        }
+    }
+}

test/rpc-server/simplify-implication/trivial-unknown/consequent.json

@@ -0,0 +1,12 @@
+{
+    "format": "KORE",
+    "version": 1,
+    "term": {
+        "tag": "EVar",
+        "name": "X",
+        "sort": {
+            "tag": "SortVar",
+            "name": "S"
+        }
+    }
+}

test/rpc-server/simplify-implication/trivial-unknown/definition.kore

@@ -0,0 +1 @@
+../../resources/empty/definition.kore

test/rpc-server/simplify-implication/trivial-unknown/response.golden

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":1,"result":{"validity":{"tag":"implication-unknown","contents":{"tag":"matching-unknown","contents":[{"format":"KORE","version":1,"term":{"tag":"EVar","name":"X","sort":{"tag":"SortVar","name":"S"}}},{"format":"KORE","version":1,"term":{"tag":"EVar","name":"X","sort":{"tag":"SortVar","name":"S"}}}]}}}}