Skip to content

Commit e5a921f

Browse files
goodlyrottenapplegoodlyrottenapple
authored
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.
1 parent be64ead commit e5a921f

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

50 files changed

+97685
-2
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -495,7 +495,7 @@ respond stateVar request =
495495
(Right newPreds, _) ->
496496
if all (== Pattern.Predicate TrueBool) newPreds
497497
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
498-
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains"
498+
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
499499
(Left other, _) ->
500500
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
501501

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

Lines changed: 73985 additions & 0 deletions
Large diffs are not rendered by default.

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

Lines changed: 2685 additions & 0 deletions
Large diffs are not rendered by default.

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

Lines changed: 5381 additions & 0 deletions
Large diffs are not rendered by default.

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 61298,
4+
"error": {
5+
"code": 4,
6+
"data": {
7+
"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)"
8+
},
9+
"message": "Implication check error"
10+
}
11+
}

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

Lines changed: 7065 additions & 0 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-implies-issue-3941/state-001.send

Lines changed: 1 addition & 0 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-implies/response-0->1.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
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/test-implies/response-0->T.booster-dev

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": "4420703856-001",
4+
"error": {
5+
"code": 2,
6+
"data": [
7+
{
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "Top",
13+
"sort": {
14+
"tag": "SortApp",
15+
"name": "SortInt",
16+
"args": []
17+
}
18+
}
19+
},
20+
"error": "Pattern must contain at least one term"
21+
}
22+
],
23+
"message": "Could not verify pattern"
24+
}
25+
}

‎booster/test/rpc-integration/test-implies/response-0->T.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
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":[]}}}}}}

‎booster/test/rpc-integration/test-implies/response-X->0.booster-dev

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": "4420567456-001",
4+
"error": {
5+
"code": 4,
6+
"data": {
7+
"error": "match remainder: \"0\" == x:SortInt{}"
8+
},
9+
"message": "Implication check error"
10+
}
11+
}

‎booster/test/rpc-integration/test-implies/response-X->0.json

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": "4420567456-001",
4+
"result": {
5+
"valid": false,
6+
"implication": {
7+
"format": "KORE",
8+
"version": 1,
9+
"term": {
10+
"tag": "Implies",
11+
"sort": {
12+
"tag": "SortApp",
13+
"name": "SortInt",
14+
"args": []
15+
},
16+
"first": {
17+
"tag": "EVar",
18+
"name": "x",
19+
"sort": {
20+
"tag": "SortApp",
21+
"name": "SortInt",
22+
"args": []
23+
}
24+
},
25+
"second": {
26+
"tag": "DV",
27+
"sort": {
28+
"tag": "SortApp",
29+
"name": "SortInt",
30+
"args": []
31+
},
32+
"value": "0"
33+
}
34+
}
35+
},
36+
"condition": {
37+
"substitution": {
38+
"format": "KORE",
39+
"version": 1,
40+
"term": {
41+
"tag": "Equals",
42+
"argSort": {
43+
"tag": "SortApp",
44+
"name": "SortInt",
45+
"args": []
46+
},
47+
"sort": {
48+
"tag": "SortApp",
49+
"name": "SortInt",
50+
"args": []
51+
},
52+
"first": {
53+
"tag": "EVar",
54+
"name": "x",
55+
"sort": {
56+
"tag": "SortApp",
57+
"name": "SortInt",
58+
"args": []
59+
}
60+
},
61+
"second": {
62+
"tag": "DV",
63+
"sort": {
64+
"tag": "SortApp",
65+
"name": "SortInt",
66+
"args": []
67+
},
68+
"value": "0"
69+
}
70+
}
71+
},
72+
"predicate": {
73+
"format": "KORE",
74+
"version": 1,
75+
"term": {
76+
"tag": "Top",
77+
"sort": {
78+
"tag": "SortApp",
79+
"name": "SortInt",
80+
"args": []
81+
}
82+
}
83+
}
84+
}
85+
}
86+
}

‎booster/test/rpc-integration/test-implies/response-X->T.booster-dev

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": "4420498928-001",
4+
"error": {
5+
"code": 2,
6+
"data": [
7+
{
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "Top",
13+
"sort": {
14+
"tag": "SortApp",
15+
"name": "SortInt",
16+
"args": []
17+
}
18+
}
19+
},
20+
"error": "Pattern must contain at least one term"
21+
}
22+
],
23+
"message": "Could not verify pattern"
24+
}
25+
}

‎booster/test/rpc-integration/test-implies/response-X->T.json

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": "4420498928-001",
4+
"result": {
5+
"valid": true,
6+
"implication": {
7+
"format": "KORE",
8+
"version": 1,
9+
"term": {
10+
"tag": "Implies",
11+
"sort": {
12+
"tag": "SortApp",
13+
"name": "SortInt",
14+
"args": []
15+
},
16+
"first": {
17+
"tag": "EVar",
18+
"name": "X",
19+
"sort": {
20+
"tag": "SortApp",
21+
"name": "SortInt",
22+
"args": []
23+
}
24+
},
25+
"second": {
26+
"tag": "Top",
27+
"sort": {
28+
"tag": "SortApp",
29+
"name": "SortInt",
30+
"args": []
31+
}
32+
}
33+
}
34+
},
35+
"condition": {
36+
"substitution": {
37+
"format": "KORE",
38+
"version": 1,
39+
"term": {
40+
"tag": "Top",
41+
"sort": {
42+
"tag": "SortApp",
43+
"name": "SortInt",
44+
"args": []
45+
}
46+
}
47+
},
48+
"predicate": {
49+
"format": "KORE",
50+
"version": 1,
51+
"term": {
52+
"tag": "Top",
53+
"sort": {
54+
"tag": "SortApp",
55+
"name": "SortInt",
56+
"args": []
57+
}
58+
}
59+
}
60+
}
61+
}
62+
}

‎booster/test/rpc-integration/test-implies/response-X->X.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc":"2.0","id":"4420580224-001","result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"EVar","name":"x","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"EVar","name":"x","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":[]}}}}}}

‎booster/test/rpc-integration/test-implies/response-fail-0->X.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
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/test-implies/response-fail-X->Y.booster-dev

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": "4420575472-001",
4+
"result": {
5+
"valid": true,
6+
"implication": {
7+
"format": "KORE",
8+
"version": 1,
9+
"term": {
10+
"tag": "Implies",
11+
"sort": {
12+
"tag": "SortApp",
13+
"name": "SortInt",
14+
"args": []
15+
},
16+
"first": {
17+
"tag": "EVar",
18+
"name": "x",
19+
"sort": {
20+
"tag": "SortApp",
21+
"name": "SortInt",
22+
"args": []
23+
}
24+
},
25+
"second": {
26+
"tag": "EVar",
27+
"name": "y",
28+
"sort": {
29+
"tag": "SortApp",
30+
"name": "SortInt",
31+
"args": []
32+
}
33+
}
34+
}
35+
},
36+
"condition": {
37+
"substitution": {
38+
"format": "KORE",
39+
"version": 1,
40+
"term": {
41+
"tag": "And",
42+
"sort": {
43+
"tag": "SortApp",
44+
"name": "SortInt",
45+
"args": []
46+
},
47+
"patterns": [
48+
{
49+
"tag": "Equals",
50+
"argSort": {
51+
"tag": "SortApp",
52+
"name": "SortInt",
53+
"args": []
54+
},
55+
"sort": {
56+
"tag": "SortApp",
57+
"name": "SortInt",
58+
"args": []
59+
},
60+
"first": {
61+
"tag": "EVar",
62+
"name": "y",
63+
"sort": {
64+
"tag": "SortApp",
65+
"name": "SortInt",
66+
"args": []
67+
}
68+
},
69+
"second": {
70+
"tag": "EVar",
71+
"name": "x",
72+
"sort": {
73+
"tag": "SortApp",
74+
"name": "SortInt",
75+
"args": []
76+
}
77+
}
78+
}
79+
]
80+
}
81+
},
82+
"predicate": {
83+
"format": "KORE",
84+
"version": 1,
85+
"term": {
86+
"tag": "Top",
87+
"sort": {
88+
"tag": "SortApp",
89+
"name": "SortInt",
90+
"args": []
91+
}
92+
}
93+
}
94+
}
95+
}
96+
}

‎booster/test/rpc-integration/test-implies/response-fail-X->Y.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc":"2.0","id":"4420575472-001","error":{"code":4,"data":{"context":["LHS: Configx:SortInt{}","RHS: Configy:SortInt{}","existentials: []"],"error":"The RHS must not have free variables not present in the LHS: Configy"},"message":"Implication check error"}}

‎booster/test/rpc-integration/test-implies/state-0->1.send

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc": "2.0", "id": "4420705104-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "1"}}}}

‎booster/test/rpc-integration/test-implies/state-0->T.send

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc": "2.0", "id": "4420703856-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "Top", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}

‎booster/test/rpc-integration/test-implies/state-X->0.send

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc": "2.0", "id": "4420567456-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}}}

‎booster/test/rpc-integration/test-implies/state-X->T.send

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc": "2.0", "id": "4420498928-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "X", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "Top", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}

‎booster/test/rpc-integration/test-implies/state-X->X.send

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc": "2.0", "id": "4420580224-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}

‎booster/test/rpc-integration/test-implies/state-fail-0->X.send

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc": "2.0", "id": "4420705104-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "1"}}}}

‎booster/test/rpc-integration/test-implies/state-fail-X->Y.send

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"jsonrpc": "2.0", "id": "4420575472-001", "method": "implies", "params": {"antecedent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "x", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}, "consequent": {"format": "KORE", "version": 1, "term": {"tag": "EVar", "name": "y", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}}}}

0 commit comments

Comments
 (0)