3956 branching on complete conditions in Booster #4058
Merged
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
geo2a
force-pushed
the
3956-booster-rewrite-rule-remainders
branch
6 times, most recently
from
0935540 to
3ba2063
Compare
geo2a
force-pushed
the
3956-booster-rewrite-rule-remainders
branch
from
13f5fc8 to
82c6764
Compare
geo2a
added a commit
that referenced
this pull request
Oct 23, 2024
Fixes #4059 This PR improves Booster's handling of substitutions. ## Summary Substitutions are special predicates: equations where the LHS is a variable, for example `VAR ==Int TERM`. See `Booster.Syntax.Json.Internalise.mbSubstitution` for the exact specification of what is considered to be a substitution. This PR changes the `Pattern` type to explicitly carry these special substitution predicates: ```diff +type Substitution = Map Variable Term + -- | A term (configuration) constrained by a number of predicates. data Pattern = Pattern { term :: Term , constraints :: !(Set Predicate) + , substitution :: Substitution , ceilConditions :: ![Ceil] } deriving stock (Eq, Ord, Show, Generic, Data) ``` Substitution may appear out of three places: - sent in the request body - ensured as a post condition of a rewrite rule - **NOT IMPLEMENTED** learned from the branching condition --- this is something that will be added as part of #4058 The first source is handled by the pattern internalisation code. The second and third sources are different, as the pattern has already been internalised. All this sources can also produce generic (i.e. non-substitution) constrains that should be added into the `constrains` set of a `Pattern`. Substitutions, when produces, should be applied to the `term` of the `Pattern` and added to the `substitution` field. This PR makes sure we use the same code path for separating substitutions from generic predicates everywhere. We use `Booster.Syntax.Json.Internalise.mbSubstitution.mkSubstitution` to take care of cyclic, which are broken up, and duplicate bindings, which are treated as constraints. With these changes, we can harmonize many (but not all) specialisations of the integrations test responses, i.e. we do not need many of the `*.booster-dev` and `*.kore-rpc-dev` response files. ## Changes to pattern simplification code As the `Pattern` type has changed, we must adapt the `ApplyEquations.evaluatePattern` and `ApplyEquations.evaluatePattern'` functions to: - consider `substitutions` as known truth together with all other constraints (that's what we did before) - simplify the substitution We achieve that by doing the following: - convert the substitution into equalities and assume it as know truth - when constructing the new, simplified pattern, use the same code as when internalising a pattern to partition predicates into the substitution and non-substitution ones ## Changes to rewrite rule application code The `Pattern.Rewrite.applyRule` function has been changed to: - consider `substiontion` as known truth together with all other constraints (that's what we did before) when checking requires/ensures - extract the substitution from the ensured conditions and add it to the rewritten pattern --------- Co-authored-by: github-actions <[email protected]>
geo2a
force-pushed
the
3956-booster-rewrite-rule-remainders
branch
4 times, most recently
from
711637d to
8994bcb
Compare
Regenerate a test output
geo2a
force-pushed
the
3956-booster-rewrite-rule-remainders
branch
from
8994bcb to
36419fa
Compare
geo2a
changed the title
|
One thing unclear from the PR description: in the case where the group of rules is incomplete, but htere are no other rules in lower priority buckets, do we still fallback to Kore or do we return the branching + the branch into the stuck state with the remainder? Also, it would be good to post performance numbers for this if possible. Are there any tests which exercise this new code in KEVM or Kontrol? |
jberthold
reviewed
Oct 28, 2024
|
No difference in KEVM performance at 691f19c Test with the Note that the KEVM test suite does not show a performance improvement because the proofs almost don't branch. |
|
I anticipate the BMC-proofs of looping code to benefit the most. For example, I ran the The version from Kontrol poetry run kontrol prove --match-test 'BMCLoopsTest.test_bmc(uint256)' --bmc-depth 10 --reinit
✨ PROOF PASSED ✨ test%BMCLoopsTest.test_bmc(uint256):12
⏳ Time: 5m 21s ⏳The version from this branch took 4m 13s: KORE_RPC_OPTS='--fallback-on Aborted' poetry run kontrol prove --match-test 'BMCLoopsTest.test_bmc(uint256)' --bmc-depth 10 --reinit --kore-rpc-command "$KRB_REM"
✨ PROOF PASSED ✨ test%BMCLoopsTest.test_bmc(uint256):11
⏳ Time: 4m 13s ⏳Note Running the Kontrol performance tests now, though I expect the difference there to show less prominently, as most of the tests are short-running, and the BMC tests are ran with |
|
Kontrol tests are extremely noisy and have several tests that show up as failing on both Feature branch was ran with
|
|
@ehildenb answering your questions:
if any rules apply but there is a SAT remainder predicate, then Booster will abort rewriting and we will get a fallback to Kore in
I've posted the numbers for KEVM and Kontrol. Unfortunately, neither test suite is representative, and I'd argue that the Kontrol results may not be 100% reliable. I've manually ran the |
geo2a
added a commit
that referenced
this pull request
Oct 28, 2024
Fixes #4059 This PR improves Booster's handling of substitutions. ## Summary Substitutions are special predicates: equations where the LHS is a variable, for example `VAR ==Int TERM`. See `Booster.Syntax.Json.Internalise.mbSubstitution` for the exact specification of what is considered to be a substitution. This PR changes the `Pattern` type to explicitly carry these special substitution predicates: ```diff +type Substitution = Map Variable Term + -- | A term (configuration) constrained by a number of predicates. data Pattern = Pattern { term :: Term , constraints :: !(Set Predicate) + , substitution :: Substitution , ceilConditions :: ![Ceil] } deriving stock (Eq, Ord, Show, Generic, Data) ``` Substitution may appear out of three places: - sent in the request body - ensured as a post condition of a rewrite rule - **NOT IMPLEMENTED** learned from the branching condition --- this is something that will be added as part of #4058 The first source is handled by the pattern internalisation code. The second and third sources are different, as the pattern has already been internalised. All this sources can also produce generic (i.e. non-substitution) constrains that should be added into the `constrains` set of a `Pattern`. Substitutions, when produces, should be applied to the `term` of the `Pattern` and added to the `substitution` field. This PR makes sure we use the same code path for separating substitutions from generic predicates everywhere. We use `Booster.Syntax.Json.Internalise.mbSubstitution.mkSubstitution` to take care of cyclic, which are broken up, and duplicate bindings, which are treated as constraints. With these changes, we can harmonize many (but not all) specialisations of the integrations test responses, i.e. we do not need many of the `*.booster-dev` and `*.kore-rpc-dev` response files. ## Changes to pattern simplification code As the `Pattern` type has changed, we must adapt the `ApplyEquations.evaluatePattern` and `ApplyEquations.evaluatePattern'` functions to: - consider `substitutions` as known truth together with all other constraints (that's what we did before) - simplify the substitution We achieve that by doing the following: - convert the substitution into equalities and assume it as know truth - when constructing the new, simplified pattern, use the same code as when internalising a pattern to partition predicates into the substitution and non-substitution ones ## Changes to rewrite rule application code The `Pattern.Rewrite.applyRule` function has been changed to: - consider `substiontion` as known truth together with all other constraints (that's what we did before) when checking requires/ensures - extract the substitution from the ensured conditions and add it to the rewritten pattern --------- Co-authored-by: github-actions <[email protected]>
jberthold
approved these changes
Oct 29, 2024
| @@ -2,7 +2,6 @@ set -eux | |||
|
|
|||
| SCRIPT_DIR=$(dirname $0) | |||
| PLUGIN_DIR=${PLUGIN_DIR:-""} | |||
| SECP=${SECP256K1_DIR:-/usr} | |||
There was a problem hiding this comment.
We also still have this in foundry-bug-report.kompile, BTW...
booster/test/rpc-integration/test-remainder-predicates/README.md
Outdated
Show resolved
Hide resolved
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
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:
requiresclause of a rule, we compute the remainder conditionRULE_REMof that attempted, which is the semantically-checked subset of the required conjunctsPwhich unclear after checking its entailment form the pattern's constrainsPC, meaning that (PC /\ P, PC /\ not P) is (SAT, SAT) or any of the two queries were UNKNOWNnot RULE_REM_iand conjunct them. This the groups remainder conditionGROUP_REM == not RULE_REM_1 /\ not RULE_REM_2 /\ ... /\ not RULE_REM_nGROUP_REMfor satisfiablity.GROUP_REMcondition 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.This behaviour is active by default in
booster-devand can be enabled inkore-rpc-boosterwith the flag--fallback-on Aborted,Stuck(the default isAborted,Stuck,Branching). Note that with the default reasons, the behaviour ofkore-rpc-boosteris functionally the same, but operationally slightly different: InProxy.hs, Booster may not returnBranching, and the fallback logic will confirm that Kore returnsBranchingas well, flagging any differences in the[proxy]logs (see Proxy.hs#L391).TODO: we need a better flag to enabled branching in Booster, as giving a
--fallback-on Aborted,Stuckis 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 and test-remainder-predicates for a series of integrations tests that cover the behaviour of
booster-devandkore-rpc-booster.