Skip to content

Commit

Permalink
Revert "Do not simplify before calling kore-rpc #362" (#403)
Browse files Browse the repository at this point in the history 
Revert #362 ~and #377~

* #362 causes Kore to return spurious branches when branching at depth
0. It looks like we must simplify the fallback state, because Kore will
not do it in this case. Alternatively, we need to modify Kore to call
the simplifier in the input state.
* ~#377 causes #401. In the state that is simplified to Bottom by
`kore-rpc-booster` there's a number of `==K` between `Bytes` functions
and `Bytes` domain value. It may be that our new `==K` simplifier on
Booster is not doing the right thing. It also may be that it does! Needs
further investigation.~ this has been fixed in #404

---------

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
  • Loading branch information
@geo2a @jberthold
geo2a and jberthold authored Dec 7, 2023
1 parent e6752d1 commit 52fffaf
Show file tree
Hide file tree
Showing 3 changed files with 356 additions and 361 deletions.
282 changes: 138 additions & 144 deletions test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,129 +9,177 @@
"format": "KORE",
"version": 1,
"term": {
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
"name": "inj",
"sorts": [
{
"tag": "App",
"name": "inj",
"sorts": [
{
"tag": "SortApp",
"name": "SortState",
"args": []
},
{
"tag": "SortApp",
"name": "SortKItem",
"args": []
}
],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"value": "d"
}
]
"tag": "SortApp",
"name": "SortState",
"args": []
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"tag": "SortApp",
"name": "SortKItem",
"args": []
}
],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortState",
"args": []
},
"value": "d"
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'int'-GT-'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
"tag": "App",
"name": "Lbl'-LT-'int'-GT-'",
"sorts": [],
"args": [
{
"tag": "Equals",
"argSort": {
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortInt",
"args": []
},
}
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"name": "SortInt",
"args": []
},
"first": {
"value": "0"
}
]
}
]
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortInt",
"args": []
},
"value": "true"
},
"second": {
"value": "0"
}
]
}
},
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "LblnotBool'Unds'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
"sorts": [],
Expand All @@ -156,62 +204,8 @@
}
]
}
},
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "LblnotBool'Unds'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
]
]
}
}
]
}
Expand Down
Loading

0 comments on commit 52fffaf

Please sign in to comment.