From 83ea3fafe00d85c32708f17734d83e497a579b5d Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 28 Jun 2023 10:41:55 +0200 Subject: [PATCH 01/13] Add 'simplify-implication' endpoint --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 27 +++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 81ff1aa9d5..092b59e1b8 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 (SimplifyImplies <$>) parseJSON parseParams "cancel" = Just $ const $ return Cancel parseParams _ = Nothing @@ -147,16 +148,15 @@ data Condition = Condition (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] Condition -data ImpliesResult = ImpliesResult - { implication :: KoreJson - , satisfiable :: Bool - , condition :: Maybe Condition +data SimplifyImpliesResult = SimplifyImpliesResult + { satisfiable :: SatResult + , substitution :: Maybe KoreJson , logs :: Maybe [LogEntry] } deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] ImpliesResult + via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImpliesResult data SimplifyResult = SimplifyResult { state :: KoreJson @@ -176,6 +176,17 @@ data GetModelResult = GetModelResult (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] GetModelResult +data ImpliesResult = ImpliesResult + { implication :: KoreJson + , satisfiable :: Bool + , condition :: Maybe Condition + , logs :: Maybe [LogEntry] + } + deriving stock (Generic, Show, Eq) + deriving + (FromJSON, ToJSON) + via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] ImpliesResult + data SatResult = Sat | Unsat @@ -193,6 +204,7 @@ data APIMethod | SimplifyM | AddModuleM | GetModelM + | SimplifyImpliesM deriving stock (Eq, Ord, Show, Enum) type family APIPayload (api :: APIMethod) (r :: ReqOrRes) where @@ -206,6 +218,8 @@ type family APIPayload (api :: APIMethod) (r :: ReqOrRes) where APIPayload 'AddModuleM 'Res = () APIPayload 'GetModelM 'Req = GetModelRequest APIPayload 'GetModelM 'Res = GetModelResult + APIPayload 'SimplifyImpliesM 'Req = ImpliesRequest + APIPayload 'SimplifyImpliesM 'Res = SimplifyImpliesResult data API (r :: ReqOrRes) where Execute :: APIPayload 'ExecuteM r -> API r @@ -213,6 +227,7 @@ data API (r :: ReqOrRes) where Simplify :: APIPayload 'SimplifyM r -> API r AddModule :: APIPayload 'AddModuleM r -> API r GetModel :: APIPayload 'GetModelM r -> API r + SimplifyImplies :: APIPayload 'SimplifyImpliesM r -> API r Cancel :: API 'Req deriving stock instance Show (API 'Req) @@ -227,6 +242,7 @@ instance ToJSON (API 'Res) where Simplify payload -> toJSON payload AddModule payload -> toJSON payload GetModel payload -> toJSON payload + SimplifyImplies payload -> toJSON payload instance Pretty.Pretty (API 'Req) where pretty = \case @@ -235,6 +251,7 @@ instance Pretty.Pretty (API 'Req) where Simplify _ -> "simplify" AddModule _ -> "add-module" GetModel _ -> "get-model" + SimplifyImplies _ -> "simplify-implication" Cancel -> "cancel" rpcJsonConfig :: PrettyJson.Config From e919814d44bb458d8d540479c10f2ab839114e70 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 25 Jul 2023 16:52:04 +0200 Subject: [PATCH 02/13] Return NotImplemented for SimplifyImplies --- kore/src/Kore/JsonRpc.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index 628c90c420..28d3ffce06 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -477,7 +477,7 @@ respond serverState moduleName runSMT = PatternJson.fromSubstitution sort $ Substitution.mapVariables getRewritingVariable subst } - + SimplifyImplies _ -> pure . Left $ Kore.JsonRpc.Error.notImplemented -- this case is only reachable if the cancel appeared as part of a batch request Cancel -> pure $ Left cancelUnsupportedInBatchMode where From 10196188ab179c91d424d08014fb4ee16c7912ea Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 25 Jul 2023 17:14:05 +0200 Subject: [PATCH 03/13] Re-order types to minimize diff --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 092b59e1b8..6c3a9a85d5 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -148,15 +148,16 @@ data Condition = Condition (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] Condition -data SimplifyImpliesResult = SimplifyImpliesResult - { satisfiable :: SatResult - , substitution :: Maybe KoreJson +data ImpliesResult = ImpliesResult + { implication :: KoreJson + , satisfiable :: Bool + , condition :: Maybe Condition , logs :: Maybe [LogEntry] } deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImpliesResult + via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] ImpliesResult data SimplifyResult = SimplifyResult { state :: KoreJson @@ -176,16 +177,15 @@ data GetModelResult = GetModelResult (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] GetModelResult -data ImpliesResult = ImpliesResult - { implication :: KoreJson - , satisfiable :: Bool - , condition :: Maybe Condition +data SimplifyImpliesResult = SimplifyImpliesResult + { satisfiable :: SatResult + , substitution :: Maybe KoreJson , logs :: Maybe [LogEntry] } deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] ImpliesResult + via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImpliesResult data SatResult = Sat From 32dbb6444bc71d6f42f07b0349c56d761bc40c92 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 8 Aug 2023 12:21:03 +0200 Subject: [PATCH 04/13] Rename `SimplifyImplies` to `SimplifyImplication` for consistency --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 6c3a9a85d5..c63eaee877 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -99,7 +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 (SimplifyImplies <$>) parseJSON + parseParams "simplify-implication" = Just $ fmap (SimplifyImplication <$>) parseJSON parseParams "cancel" = Just $ const $ return Cancel parseParams _ = Nothing @@ -177,7 +177,7 @@ data GetModelResult = GetModelResult (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] GetModelResult -data SimplifyImpliesResult = SimplifyImpliesResult +data SimplifyImplicationResult = SimplifyImplicationResult { satisfiable :: SatResult , substitution :: Maybe KoreJson , logs :: Maybe [LogEntry] @@ -185,7 +185,7 @@ data SimplifyImpliesResult = SimplifyImpliesResult deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImpliesResult + via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImplicationResult data SatResult = Sat @@ -204,7 +204,7 @@ data APIMethod | SimplifyM | AddModuleM | GetModelM - | SimplifyImpliesM + | SimplifyImplicationM deriving stock (Eq, Ord, Show, Enum) type family APIPayload (api :: APIMethod) (r :: ReqOrRes) where @@ -218,8 +218,8 @@ type family APIPayload (api :: APIMethod) (r :: ReqOrRes) where APIPayload 'AddModuleM 'Res = () APIPayload 'GetModelM 'Req = GetModelRequest APIPayload 'GetModelM 'Res = GetModelResult - APIPayload 'SimplifyImpliesM 'Req = ImpliesRequest - APIPayload 'SimplifyImpliesM 'Res = SimplifyImpliesResult + APIPayload 'SimplifyImplicationM 'Req = ImpliesRequest + APIPayload 'SimplifyImplicationM 'Res = SimplifyImplicationResult data API (r :: ReqOrRes) where Execute :: APIPayload 'ExecuteM r -> API r @@ -227,7 +227,7 @@ data API (r :: ReqOrRes) where Simplify :: APIPayload 'SimplifyM r -> API r AddModule :: APIPayload 'AddModuleM r -> API r GetModel :: APIPayload 'GetModelM r -> API r - SimplifyImplies :: APIPayload 'SimplifyImpliesM r -> API r + SimplifyImplication :: APIPayload 'SimplifyImplicationM r -> API r Cancel :: API 'Req deriving stock instance Show (API 'Req) @@ -242,7 +242,7 @@ instance ToJSON (API 'Res) where Simplify payload -> toJSON payload AddModule payload -> toJSON payload GetModel payload -> toJSON payload - SimplifyImplies payload -> toJSON payload + SimplifyImplication payload -> toJSON payload instance Pretty.Pretty (API 'Req) where pretty = \case @@ -251,7 +251,7 @@ instance Pretty.Pretty (API 'Req) where Simplify _ -> "simplify" AddModule _ -> "add-module" GetModel _ -> "get-model" - SimplifyImplies _ -> "simplify-implication" + SimplifyImplication _ -> "simplify-implication" Cancel -> "cancel" rpcJsonConfig :: PrettyJson.Config From 839fe34aac1166948b4ebb673d8c8ec506b18af0 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 8 Aug 2023 12:25:24 +0200 Subject: [PATCH 05/13] Use `ValidityResult` for additional clarity --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index c63eaee877..9336ad7217 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -180,6 +180,7 @@ data GetModelResult = GetModelResult data SimplifyImplicationResult = SimplifyImplicationResult { satisfiable :: SatResult , substitution :: Maybe KoreJson + { valid :: ValidityResult , logs :: Maybe [LogEntry] } deriving stock (Generic, Show, Eq) @@ -187,6 +188,15 @@ data SimplifyImplicationResult = SimplifyImplicationResult (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImplicationResult +data ValidityResult + = Valid + | Invalid + | ValidityUnknown + deriving stock (Generic, Show, Eq) + deriving + (FromJSON, ToJSON) + via CustomJSON '[] ValidityResult + data SatResult = Sat | Unsat From 60990abc2a94ee344de6002e2410f1c03b0c49d2 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 8 Aug 2023 12:25:46 +0200 Subject: [PATCH 06/13] Reuse the `Condition` type for substitution and constrains --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 9336ad7217..db25e1300e 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -178,9 +178,8 @@ data GetModelResult = GetModelResult via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] GetModelResult data SimplifyImplicationResult = SimplifyImplicationResult - { satisfiable :: SatResult - , substitution :: Maybe KoreJson - { valid :: ValidityResult + { validity :: ValidityResult + , condition :: Maybe Condition , logs :: Maybe [LogEntry] } deriving stock (Generic, Show, Eq) From 5b82de9c02424cb390c0bc0597ff0c85ab80f579 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 8 Aug 2023 15:55:35 +0200 Subject: [PATCH 07/13] Specify implication validity result --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 30 ++++++++++++++++++------ 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index db25e1300e..921dfd1873 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -178,8 +178,7 @@ data GetModelResult = GetModelResult via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] GetModelResult data SimplifyImplicationResult = SimplifyImplicationResult - { validity :: ValidityResult - , condition :: Maybe Condition + { validity :: ImplicationValidityResult , logs :: Maybe [LogEntry] } deriving stock (Generic, Show, Eq) @@ -187,14 +186,31 @@ data SimplifyImplicationResult = SimplifyImplicationResult (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImplicationResult -data ValidityResult - = Valid - | Invalid - | ValidityUnknown +data ImplicationValidityResult + = -- | implication is valid, constrained substitution returned + ImplicationValid KoreJson + | -- | implication is invalid, explains why + ImplicationInvalid ImplicationInvalidReason + | -- | implication is unknown, explains why + ImplicationUnknwon ImplicationInvalidReason + deriving stock (Generic, Show, Eq) + deriving + (FromJSON, ToJSON) + via CustomJSON '[] ImplicationValidityResult + +data ImplicationInvalidReason + = ImplicationTermsDontUnify KoreJson + | ImplicationConstraintSubsumptionFailed KoreJson + deriving stock (Generic, Show, Eq) + deriving + (FromJSON, ToJSON) + via CustomJSON '[] ImplicationInvalidReason + +data ImplicationUnknwonReason = ImplicationConstraintSubsumptionUnknown KoreJson deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[] ValidityResult + via CustomJSON '[] ImplicationUnknwonReason data SatResult = Sat From 501ad4cce61b71589abd95c0b02d818df955f78f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 8 Aug 2023 16:15:51 +0200 Subject: [PATCH 08/13] Fix typo --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 921dfd1873..145f6fd7b7 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -192,7 +192,7 @@ data ImplicationValidityResult | -- | implication is invalid, explains why ImplicationInvalid ImplicationInvalidReason | -- | implication is unknown, explains why - ImplicationUnknwon ImplicationInvalidReason + ImplicationUnknown ImplicationInvalidReason deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) @@ -206,11 +206,11 @@ data ImplicationInvalidReason (FromJSON, ToJSON) via CustomJSON '[] ImplicationInvalidReason -data ImplicationUnknwonReason = ImplicationConstraintSubsumptionUnknown KoreJson +data ImplicationUnknownReason = ImplicationConstraintSubsumptionUnknown KoreJson deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[] ImplicationUnknwonReason + via CustomJSON '[] ImplicationUnknownReason data SatResult = Sat From 27c81b4ff58095a919c5888815891f07dbea983f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 9 Aug 2023 09:37:24 +0200 Subject: [PATCH 09/13] Make RPC implication types match the ones in Booster --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 145f6fd7b7..eca173e9ba 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -192,21 +192,23 @@ data ImplicationValidityResult | -- | implication is invalid, explains why ImplicationInvalid ImplicationInvalidReason | -- | implication is unknown, explains why - ImplicationUnknown ImplicationInvalidReason + ImplicationUnknown ImplicationUnknownReason deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) via CustomJSON '[] ImplicationValidityResult data ImplicationInvalidReason - = ImplicationTermsDontUnify KoreJson - | ImplicationConstraintSubsumptionFailed KoreJson + = MatchingFailed KoreJson + | ConstraintSubsumptionFailed KoreJson deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) via CustomJSON '[] ImplicationInvalidReason -data ImplicationUnknownReason = ImplicationConstraintSubsumptionUnknown KoreJson +data ImplicationUnknownReason + = MatchingUnknown KoreJson + | ConstraintSubsumptionUnknown KoreJson deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) From 3f22ee19cc591ce88cb8130c5442e9b344498729 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 9 Aug 2023 10:25:37 +0200 Subject: [PATCH 10/13] Reshuffle SimplifyImplicationResult --- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index eca173e9ba..b2a8f38137 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -179,6 +179,7 @@ data GetModelResult = GetModelResult data SimplifyImplicationResult = SimplifyImplicationResult { validity :: ImplicationValidityResult + , substitution :: Maybe KoreJson , logs :: Maybe [LogEntry] } deriving stock (Generic, Show, Eq) @@ -187,8 +188,8 @@ data SimplifyImplicationResult = SimplifyImplicationResult via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImplicationResult data ImplicationValidityResult - = -- | implication is valid, constrained substitution returned - ImplicationValid KoreJson + = -- | implication is valid + ImplicationValid | -- | implication is invalid, explains why ImplicationInvalid ImplicationInvalidReason | -- | implication is unknown, explains why @@ -199,16 +200,20 @@ data ImplicationValidityResult via CustomJSON '[] ImplicationValidityResult data ImplicationInvalidReason - = MatchingFailed KoreJson - | ConstraintSubsumptionFailed KoreJson + = -- | 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 '[] ImplicationInvalidReason data ImplicationUnknownReason - = MatchingUnknown KoreJson - | ConstraintSubsumptionUnknown KoreJson + = -- | 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) From 28bbb0a813d2dd1f182e6346caa1529972c2780f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 10 Aug 2023 10:45:44 +0200 Subject: [PATCH 11/13] Add an implementation stub of `simplify-implication` to `kore-rpc` --- kore/src/Kore/JsonRpc.hs | 8 +++++++- test/rpc-server/runTests.py | 18 ++++++++++++++++++ .../implied-trivial/README.md | 1 + .../implied-trivial/antecedent.json | 12 ++++++++++++ .../implied-trivial/consequent.json | 12 ++++++++++++ .../implied-trivial/definition.kore | 1 + .../implied-trivial/response.golden | 1 + 7 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 test/rpc-server/simplify-implication/implied-trivial/README.md create mode 100644 test/rpc-server/simplify-implication/implied-trivial/antecedent.json create mode 100644 test/rpc-server/simplify-implication/implied-trivial/consequent.json create mode 120000 test/rpc-server/simplify-implication/implied-trivial/definition.kore create mode 100644 test/rpc-server/simplify-implication/implied-trivial/response.golden diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index ab914ff6d2..81dfd06eb3 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -477,7 +477,13 @@ respond serverState moduleName runSMT = PatternJson.fromSubstitution sort $ Substitution.mapVariables getRewritingVariable subst } - SimplifyImplication _ -> pure . Left $ Kore.JsonRpc.Error.notImplemented + 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/implied-trivial/README.md b/test/rpc-server/simplify-implication/implied-trivial/README.md new file mode 100644 index 0000000000..e7727ec570 --- /dev/null +++ b/test/rpc-server/simplify-implication/implied-trivial/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/implied-trivial/antecedent.json b/test/rpc-server/simplify-implication/implied-trivial/antecedent.json new file mode 100644 index 0000000000..7e5376a9eb --- /dev/null +++ b/test/rpc-server/simplify-implication/implied-trivial/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/implied-trivial/consequent.json b/test/rpc-server/simplify-implication/implied-trivial/consequent.json new file mode 100644 index 0000000000..7e5376a9eb --- /dev/null +++ b/test/rpc-server/simplify-implication/implied-trivial/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/implied-trivial/definition.kore b/test/rpc-server/simplify-implication/implied-trivial/definition.kore new file mode 120000 index 0000000000..89dde956b8 --- /dev/null +++ b/test/rpc-server/simplify-implication/implied-trivial/definition.kore @@ -0,0 +1 @@ +../../resources/empty/definition.kore \ No newline at end of file diff --git a/test/rpc-server/simplify-implication/implied-trivial/response.golden b/test/rpc-server/simplify-implication/implied-trivial/response.golden new file mode 100644 index 0000000000..73df4e8265 --- /dev/null +++ b/test/rpc-server/simplify-implication/implied-trivial/response.golden @@ -0,0 +1 @@ +{"jsonrpc":"2.0","id":1,"result":{"validity":{"tag":"ImplicationUnknown","contents":{"tag":"MatchingUnknown","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"}}}]}}}} From 04285279c2f0ec0d06457a6b8ff335a1f85dab0e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 10 Aug 2023 11:30:10 +0200 Subject: [PATCH 12/13] Add `simplify-implication` docs --- docs/2022-07-18-JSON-RPC-Server-API.md | 121 +++++++++++++++++++++++++ 1 file changed, 121 insertions(+) diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 4aa914bd7e..2ccf5ef2e7 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": "ImplicationValid"}, + "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": "ImplicationInvalid", + "contents": {"tag": "MatchingFailed", + "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": "ImplicationInvalid", + "contents": {"tag": "ConstraintSubsumptionFailed", + "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": "ImplicationUnknown", + "contents": {"tag": "MatchingUnknown", + "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": "ImplicationUnknown", + "contents": {"tag": "ConstraintSubsumptionUnknown", + "contents": {"tag": "ConstraintSubsumptionFailed", + "contents": {"format": "KORE", "version": 1, "term": {}} + }}, + "substitution": {"format": "KORE", "version": 1, "term": {}}, + } +} +``` + ## Add-module ### Request From 6a712b27bd3f6a6de2129853a9ca541dd859aa33 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 10 Aug 2023 17:10:21 +0200 Subject: [PATCH 13/13] Make ImplicationValidity tags lower-case --- docs/2022-07-18-JSON-RPC-Server-API.md | 20 +++++++++---------- kore-rpc-types/src/Kore/JsonRpc/Types.hs | 6 +++--- .../implied-trivial/response.golden | 1 - .../README.md | 0 .../antecedent.json | 0 .../consequent.json | 0 .../definition.kore | 0 .../trivial-unknown/response.golden | 1 + 8 files changed, 14 insertions(+), 14 deletions(-) delete mode 100644 test/rpc-server/simplify-implication/implied-trivial/response.golden rename test/rpc-server/simplify-implication/{implied-trivial => trivial-unknown}/README.md (100%) rename test/rpc-server/simplify-implication/{implied-trivial => trivial-unknown}/antecedent.json (100%) rename test/rpc-server/simplify-implication/{implied-trivial => trivial-unknown}/consequent.json (100%) rename test/rpc-server/simplify-implication/{implied-trivial => trivial-unknown}/definition.kore (100%) create mode 100644 test/rpc-server/simplify-implication/trivial-unknown/response.golden diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 2ccf5ef2e7..1bea993a67 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/docs/2022-07-18-JSON-RPC-Server-API.md @@ -430,7 +430,7 @@ A constrained substitution as the result, and this is only returned if the impli "jsonrpc": "2.0", "id": 1, "result": { - "validity": {"tag": "ImplicationValid"}, + "validity": {"tag": "implication-valid"}, "substitution": {"format": "KORE", "version": 1, "term": {}}, } } @@ -445,8 +445,8 @@ Matching between antecedent and consequent configurations failed (different cons "jsonrpc": "2.0", "id": 1, "result": { - "validity": {"tag": "ImplicationInvalid", - "contents": {"tag": "MatchingFailed", + "validity": {"tag": "implication-valid", + "contents": {"tag": "matching-failed", "contents": "Shared variables: X:SortWordStack{}" }}, } @@ -462,8 +462,8 @@ Matching between antecedent and consequent configurations is successful, but con "jsonrpc": "2.0", "id": 1, "result": { - "validity": {"tag": "ImplicationInvalid", - "contents": {"tag": "ConstraintSubsumptionFailed", + "validity": {"tag": "implication-valid", + "contents": {"tag": "constraint-subsumption-failed", "contents": {"format": "KORE", "version": 1, "term": {}} }}, "substitution": {"format": "KORE", "version": 1, "term": {}}, @@ -480,8 +480,8 @@ The matching algorithm is incomplete and may return an indeterminate result. The "jsonrpc": "2.0", "id": 1, "result": { - "validity": {"tag": "ImplicationUnknown", - "contents": {"tag": "MatchingUnknown", + "validity": {"tag": "implication-unknown", + "contents": {"tag": "matching-unknown", "contents": {"first" : {"format": "KORE", "version": 1, "term": {}} ,"second" : {"format": "KORE", "version": 1, "term": {}} } @@ -499,9 +499,9 @@ If matching is successful, but the constraint solver procedure (internal, or the "jsonrpc": "2.0", "id": 1, "result": { - "validity": {"tag": "ImplicationUnknown", - "contents": {"tag": "ConstraintSubsumptionUnknown", - "contents": {"tag": "ConstraintSubsumptionFailed", + "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": {}}, diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 8758221aa2..e7cd1497f4 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -198,7 +198,7 @@ data ImplicationValidityResult deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[] ImplicationValidityResult + via CustomJSON '[ConstructorTagModifier '[CamelToKebab]] ImplicationValidityResult data ImplicationInvalidReason = -- | antecedent and consequent do not match @@ -208,7 +208,7 @@ data ImplicationInvalidReason deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[] ImplicationInvalidReason + via CustomJSON '[ConstructorTagModifier '[CamelToKebab]] ImplicationInvalidReason data ImplicationUnknownReason = -- | matching between antecedent and consequent is indeterminate, return the subterms that caused this @@ -218,7 +218,7 @@ data ImplicationUnknownReason deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[] ImplicationUnknownReason + via CustomJSON '[ConstructorTagModifier '[CamelToKebab]] ImplicationUnknownReason data SatResult = Sat diff --git a/test/rpc-server/simplify-implication/implied-trivial/response.golden b/test/rpc-server/simplify-implication/implied-trivial/response.golden deleted file mode 100644 index 73df4e8265..0000000000 --- a/test/rpc-server/simplify-implication/implied-trivial/response.golden +++ /dev/null @@ -1 +0,0 @@ -{"jsonrpc":"2.0","id":1,"result":{"validity":{"tag":"ImplicationUnknown","contents":{"tag":"MatchingUnknown","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"}}}]}}}} diff --git a/test/rpc-server/simplify-implication/implied-trivial/README.md b/test/rpc-server/simplify-implication/trivial-unknown/README.md similarity index 100% rename from test/rpc-server/simplify-implication/implied-trivial/README.md rename to test/rpc-server/simplify-implication/trivial-unknown/README.md diff --git a/test/rpc-server/simplify-implication/implied-trivial/antecedent.json b/test/rpc-server/simplify-implication/trivial-unknown/antecedent.json similarity index 100% rename from test/rpc-server/simplify-implication/implied-trivial/antecedent.json rename to test/rpc-server/simplify-implication/trivial-unknown/antecedent.json diff --git a/test/rpc-server/simplify-implication/implied-trivial/consequent.json b/test/rpc-server/simplify-implication/trivial-unknown/consequent.json similarity index 100% rename from test/rpc-server/simplify-implication/implied-trivial/consequent.json rename to test/rpc-server/simplify-implication/trivial-unknown/consequent.json diff --git a/test/rpc-server/simplify-implication/implied-trivial/definition.kore b/test/rpc-server/simplify-implication/trivial-unknown/definition.kore similarity index 100% rename from test/rpc-server/simplify-implication/implied-trivial/definition.kore rename to test/rpc-server/simplify-implication/trivial-unknown/definition.kore 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"}}}]}}}}