Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jul 30, 2024
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
3348915
Add pyk implication tests to the rpc integration test suite
goodlyrottenapple Jul 26, 2024
ab6f52e
add test from issue #3941
goodlyrottenapple Jul 26, 2024
f1fc704
fix typo
goodlyrottenapple Jul 29, 2024
5033f4f
fix typo
goodlyrottenapple Jul 29, 2024
1432ba6
format json inputs
goodlyrottenapple Jul 29, 2024
d70e890
Merge branch 'master' into sam/implication-rpc-tests
goodlyrottenapple Jul 30, 2024
cc2c034
Add readme
goodlyrottenapple Jul 30, 2024
2f4a143
Merge branch 'sam/implication-rpc-tests' of github.com:runtimeverific…
goodlyrottenapple Jul 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion booster/library/Booster/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
73,985 changes: 73,985 additions & 0 deletions booster/test/rpc-integration/resources/implies-issue-3941.kore
View file
Open in desktop

Large diffs are not rendered by default.

2,685 changes: 2,685 additions & 0 deletions booster/test/rpc-integration/resources/implies.kore
View file
Open in desktop

Large diffs are not rendered by default.

5,381 changes: 5,381 additions & 0 deletions booster/test/rpc-integration/resources/implies2.kore
View file
Open in desktop

Large diffs are not rendered by default.

11 changes: 11 additions & 0 deletions booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
}
7,065 changes: 7,065 additions & 0 deletions booster/test/rpc-integration/test-implies-issue-3941/response-001.json
View file
Open in desktop

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies-issue-3941/state-001.send
View file
Open in desktop

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-0->1.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"}}}}}
25 changes: 25 additions & 0 deletions booster/test/rpc-integration/test-implies/response-0->T.booster-dev
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-0->T.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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":[]}}}}}}
11 changes: 11 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->0.booster-dev
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"jsonrpc": "2.0",
"id": "4420567456-001",
"error": {
"code": 4,
"data": {
"error": "match remainder: \"0\" == x:SortInt{}"
},
"message": "Implication check error"
}
}
86 changes: 86 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->0.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
{
"jsonrpc": "2.0",
"id": "4420567456-001",
"result": {
"valid": false,
"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": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
}
},
"condition": {
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"first": {
"tag": "EVar",
"name": "x",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
}
}
}
25 changes: 25 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->T.booster-dev
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
{
"jsonrpc": "2.0",
"id": "4420498928-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"
}
}
62 changes: 62 additions & 0 deletions booster/test/rpc-integration/test-implies/response-X->T.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
{
"jsonrpc": "2.0",
"id": "4420498928-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": "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": []
}
}
}
}
}
}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-X->X.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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":[]}}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-fail-0->X.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"}}}}}
96 changes: 96 additions & 0 deletions booster/test/rpc-integration/test-implies/response-fail-X->Y.booster-dev
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
{
"jsonrpc": "2.0",
"id": "4420575472-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": "y",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
},
"condition": {
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"patterns": [
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"first": {
"tag": "EVar",
"name": "y",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "EVar",
"name": "x",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
]
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Top",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
}
}
}
}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/response-fail-X->Y.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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"}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-0->1.send
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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"}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-0->T.send
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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": []}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-X->0.send
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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"}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-X->T.send
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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": []}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-X->X.send
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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": []}}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-fail-0->X.send
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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"}}}}
1 change: 1 addition & 0 deletions booster/test/rpc-integration/test-implies/state-fail-X->Y.send
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +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": []}}}}}
Loading
Loading