runtimeverification / runtimeverification/haskell-backend
Booster's simplifier is unable to prune a `#Bottom` state
@jberthold is already working on this.
Since Dec 4, 2024.
- Dominant language
- Haskell
- Stars
- 224
- Forks
- 43
- PR merge metrics
- No merged PRs in 30d
Description
The integration test test-issue3764-vacuous-branch isolates a case where Booster's simplifier is unable to prune a bottom state.
When sent given the state-branch-in-zero.send request, booster-dev (and kore-rpc-booster --no-post-exec-simplify) returns a Branchingresponse, whilekore-rpc-boosterreturnsDepthBound, making two steps. This happens because kore-rpc-booster` will call Kore's simplify endpoint, which is more powerful (but much slower).
The other request, state-branch-after-one.send, is basically the same, but the state is from one step before. booster-dev branches after 1 step and kore-rpc-booster makes 3 steps.
We need to figure out exactly what allows the Kore's simplifier to prune the state. An important details is that the pruning happens not in Kore's rule unification algorithm, i.e. Kore returns Branching too. It is the simplify request that produces #Bottom in the end.
Note that https://github.com/runtimeverification/haskell-backend/pull/4020 (checking input pattern's conditions with SMT in Booster) is also not enough, i.e. even with that code Booster is unable to derive a contradiction.
To observe the relevant logs, run the following from the following from the repo root:
SERVER=$(cabal list-bin kore-rpc-booster) SERVER_OPTS="--log-context \"*>proxy>*\"" CLIENT=$(cabal list-bin kore-rpc-client) ./booster/test/rpc-integration/runDirectoryTest.sh booster/test/rpc-integration/test-issue3764-vacuous-branch
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.