diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 4aa914bd7e..1bea993a67 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/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 diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index e39f9ad676..e7cd1497f4 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/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,6 +251,8 @@ 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 @@ -214,6 +260,7 @@ data API (r :: ReqOrRes) where 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 diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index efc1e0aeb7..0d32f38a1a 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/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 diff --git a/test/rpc-server/runTests.py b/test/rpc-server/runTests.py index dd66a469b6..c6373cb7f9 100644 --- a/test/rpc-server/runTests.py +++ b/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) diff --git a/test/rpc-server/simplify-implication/trivial-unknown/README.md b/test/rpc-server/simplify-implication/trivial-unknown/README.md new file mode 100644 index 0000000000..e7727ec570 --- /dev/null +++ b/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`. diff --git a/test/rpc-server/simplify-implication/trivial-unknown/antecedent.json b/test/rpc-server/simplify-implication/trivial-unknown/antecedent.json new file mode 100644 index 0000000000..7e5376a9eb --- /dev/null +++ b/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" + } + } +} diff --git a/test/rpc-server/simplify-implication/trivial-unknown/consequent.json b/test/rpc-server/simplify-implication/trivial-unknown/consequent.json new file mode 100644 index 0000000000..7e5376a9eb --- /dev/null +++ b/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" + } + } +} diff --git a/test/rpc-server/simplify-implication/trivial-unknown/definition.kore b/test/rpc-server/simplify-implication/trivial-unknown/definition.kore new file mode 120000 index 0000000000..89dde956b8 --- /dev/null +++ b/test/rpc-server/simplify-implication/trivial-unknown/definition.kore @@ -0,0 +1 @@ +../../resources/empty/definition.kore \ No newline at end of file diff --git a/test/rpc-server/simplify-implication/trivial-unknown/response.golden b/test/rpc-server/simplify-implication/trivial-unknown/response.golden new file mode 100644 index 0000000000..c55128d689 --- /dev/null +++ b/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"}}}]}}}}