Explore the remainder branch when Booster is uncertain about rewrite rule conditions #3960
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ern + fix unit tests
geo2a
force-pushed
the
georgy/booster-remainders
branch
from
9d065d9 to
391b47c
Compare
geo2a
force-pushed
the
georgy/booster-remainders
branch
from
71ba327 to
ad42fbd
Compare
|
KEVM performance at 7bf75ea: |
geo2a
force-pushed
the
georgy/booster-remainders
branch
from
fcc8ed0 to
a580cfc
Compare
geo2a
added a commit
that referenced
this pull request
Sep 25, 2024
geo2a
added a commit
that referenced
this pull request
Oct 7, 2024
geo2a
added a commit
that referenced
this pull request
Oct 15, 2024
geo2a
added a commit
that referenced
this pull request
Oct 15, 2024
geo2a
added a commit
that referenced
this pull request
Oct 17, 2024
geo2a
added a commit
that referenced
this pull request
Oct 22, 2024
geo2a
added a commit
that referenced
this pull request
Oct 23, 2024
geo2a
added a commit
that referenced
this pull request
Oct 25, 2024
|
Closed in favor of #4058 |
geo2a
added a commit
that referenced
this pull request
Oct 29, 2024
Part of #3956 Partially subsumes #3960 This PR makes the rewrite rule application algorithm of Booster more powerful by allowing branching on *complete conditions*. The rewriting algorithm is modified: - when checking the `requires` clause of a rule, we compute the remainder condition `RULE_REM` of that attempted, which is the semantically-checked subset of the required conjuncts `P` which *unclear* after checking its entailment form the pattern's constrains `PC`, meaning that (PC /\ P, PC /\ not P) is (SAT, SAT) or any of the two queries were UNKNOWN - if that remainder is not empty, we return it's *negation* together with the result - when we are finished attempting a *priority group* of rules, we collect the negated remainder conditions `not RULE_REM_i` and conjunct them. This the groups remainder condition `GROUP_REM == not RULE_REM_1 /\ not RULE_REM_2 /\ ... /\ not RULE_REM_n` - At that point, we need to check `GROUP_REM` for satisfiablity. - **If the `GROUP_REM` condition is UNSAT, it means that this group of rules is *complete***, meaning that no other rule can possibly apply, and we do not need to even attempt applying rules of lower priority. This behaviour is the **primary contribution of this PR**. - Otherwise, if it is SAT or solver said UNKNOWN, it means that this group of rules is not complete, i.e. it does not cover the whole space of logical possibility, and we need to construct a remainder configuration, and continue attempting to apply other rules to it. If no rules remain, it means that we are stuck and the semantics is incomplete. This PR does not implement the process of descending into the remainder branch. **Booster with this PR will abort on a SAT remainder**. This behaviour is active by default in `booster-dev` and can be enabled in `kore-rpc-booster` with the flag `--fallback-on Aborted,Stuck` (the default is `Aborted,Stuck,Branching`). Note that with the default reasons, the behaviour of `kore-rpc-booster` is functionally the same, but operationally slightly different: In `Proxy.hs`, Booster may not return `Branching`, and the fallback logic will confirm that Kore returns `Branching` as well, flagging any differences in the `[proxy]` logs (see [Proxy.hs#L391](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/tools/booster/Proxy.hs#L391)). TODO: we need a better flag to enabled branching in Booster, as giving a `--fallback-on Aborted,Stuck` is really non-intuitive. Note: a naive algorithm to compute the remainder conditions would be: after applying a group of rules, take their substituted requires clauses, disjunct and negate. However, this yields a non-minimal predicate that was not simplified and syntactically filtered, potentially making it harder for the SMT solver to solve. The algorithm described above and implemented in this PR re-uses the indeterminate results obtained while applying individual rules and simplifying/checking their individual requires clauses. This logic has been originally proposed by Sam in #3960. See [remainder-predicates.k](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/test/rpc-integration/resources/remainder-predicates.k) and [test-remainder-predicates](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/test/rpc-integration/test-remainder-predicates) for a series of integrations tests that cover the behaviour of `booster-dev` and `kore-rpc-booster`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Part of #3956