Add pyk implication tests to the rpc integration test suite (#3997)

This is the first step in bringing the booster implication endpoint in
line with kore. Most of the `.booster-dev` responses will eventually be
the same/equivalent to the kore responses.

Author: goodlyrottenapple

booster/library/Booster/JsonRpc.hs

@@ -495,7 +495,7 @@ respond stateVar request =
                                             (Right newPreds, _) ->
                                                 if all (== Pattern.Predicate TrueBool) newPreds
                                                     then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
-                                                    else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains"
+                                                    else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
                                             (Left other, _) ->
                                                 pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
 

booster/test/rpc-integration/resources/implies-issue-3941.kore

@@ -0,0 +1,11 @@
+{
+    "jsonrpc": "2.0",
+    "id": 61298,
+    "error": {
+        "code": 4,
+        "data": {
+            "error": "match remainder: Map:update(VarS:SortMap{}, \"0\", \"0\") == Map:update(\n    VarS:SortMap{},\n    \"0\",\n    chop(_)_WORD_Int_Int(_+Int_(lookup(VarS:SortMap{}, \"0\"), \"1\"))\n), \"\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL...truncated\" == buf(\n    \"32\",\n    chop(_)_WORD_Int_Int(_+Int_(lookup(VarS:SortMap{}, \"0\"), \"1\"))\n)"
+        },
+        "message": "Implication check error"
+    }
+}

booster/test/rpc-integration/resources/implies.kore

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":"4420705104-001","result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}}}}}

booster/test/rpc-integration/resources/implies2.kore

@@ -0,0 +1,25 @@
+{
+    "jsonrpc": "2.0",
+    "id": "4420703856-001",
+    "error": {
+        "code": 2,
+        "data": [
+            {
+                "term": {
+                    "format": "KORE",
+                    "version": 1,
+                    "term": {
+                        "tag": "Top",
+                        "sort": {
+                            "tag": "SortApp",
+                            "name": "SortInt",
+                            "args": []
+                        }
+                    }
+                },
+                "error": "Pattern must contain at least one term"
+            }
+        ],
+        "message": "Could not verify pattern"
+    }
+}

booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":"4420703856-001","result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}}}}