Compute remainders in booster #3956
Comments
geo2a
added a commit
that referenced
this issue
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
Various issues with remainders have been identified in kore recently see #3948. These issues should not be addressed in kore due to various reasons, including kore not being actively maintained and the difficulties associated with reasoning/debugging of the kore backend. Instead, we need to implement remainder computation in booster where we can then more efficiently explore various optimisations suggested in the aforementioned issue. This issue should serve as the design document for implementing the remainder computation algorithm.
Currently, the booster aborts in the following scenarios and what i think we should do:
C(...)withf(...)wherefis a function andCis a constructor (only aborts if this happens after a round of configuration simplification)action: split the current state by
C(...) == f(...)to path constraints and continue with current rule and then try all remaining rulesC(...) =/= f(...)to path constraints and then try all remaining rulesaction:
add #Ceil(<term>)to path conditions for the sub<term>which does not preserve definedness and continueCcould not be determined to be trueaction: split the current state by
Cto path constraints and continue with current rule and then try all remaining rulesnotBool Cto path constraints and then try all remaining rulesThe changes above should mean we no longer abort and fall back to kore. However, this design is still incomplete/incorrect in the face of applying multiple rules with different priorities: https://github.com/runtimeverification/haskell-backend/blob/master/docs/2019-08-29-Remainders-for-priority-rules.md
The text was updated successfully, but these errors were encountered: