-
Notifications
You must be signed in to change notification settings - Fork 43
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
4012 evaluate pattern pruning #4020
base: master
Are you sure you want to change the base?
Conversation
71998b1
to
84b3b61
Compare
KEVM performance:
|
e8b111d
to
8312613
Compare
@@ -93,7 +93,7 @@ | |||
"name": "SortInt", | |||
"args": [] | |||
}, | |||
"value": "6" | |||
"value": "4" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The strange changes to this the output of test-collectiontest
were caused by the reuse of .json
output file by both kore-rpc-booster
and booster-dev
runs of the test. Since Booster's result is stuck
(no more rules), kore-rpc-booster
will fallback to Kore
and the result will contain Kore's preferred set ordering.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this diff really does not make much sense.
What happened to test-diamond
is: the differences between booster-dev
and kore-rpc-booster
are mostly eliminated, but some test results have to be special-cased for kore-rpc-dev
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This response (and response-branch-after-one.json) are now branching. Kore's simplifier is necessary to prune the state after jumpi.false
. It is still unclear what it going on here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would maybe just leave --post-exec-simplify
on for this test instead...
"predicate": { | ||
"format": "KORE", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a bit weird... the updated output does not have any "predicate"
any more?
There is a major slowdown in engagement proofs as a result of this PR. A I think that we might need to construct a more representative test suite. |
ceb3c1e
to
3f29753
Compare
3f29753
to
afaa394
Compare
I've removed the data in this comment as I've been running with an incorrect branch, sorry for the spam. |
I've run the
This proof seems to be special in the sense that it does not branch a single time and always stays in Booster, hence this change introduces a slowdown, as we start calling Z3 at the beginning of every execute request. It is not clear to me at that point why the slowdown is so massive. |
72d4801
to
cdce88c
Compare
With cdce88c the runtime of |
Just in case this could be useful. For me, the SAT checking points are:
I don't think there is a need to make additional checks at branching points, because there are already checks in place that Even if we cut both |
|
To measure the effect of this PR, I am running:
I am running using commit With HB version 0.1.67, which comes with that version of K (it's a bit behind, isn't it?), the result is as follows:
which is actually a record-breaking time by ~4 minutes. Using HB from this branch, commit
and it is clear that having a SAT check at the start of each request causes a substantial overhead. Here, it means that ~560 extra checks were made with respect to the TL; DR: This does not look good for real-world proofs. I think we need to really understand do we want this at all, that is, what is the worst that could happen if we actually started a request from an UNSAT state in the booster. |
Thanks @PetarMax! I'd like to re-iterate on the ask to upstream this test, perhaps partially, as to KEVM as a claim, so that we can run is as part of out performance measurement. Regarding having an RPC parameter to turn the initial constraints check off: we actually already have one we could use. It is the |
…fault: no simplification) * Introduces options `--fallback-simplify` and `--post-exec-simplify` to perform said simplifications (before fallbacks and after execute) in `kore-rpc-booster` * The old `--no-fallback-simplify` and `--no-post-exec-simplify` options are still accepted but not doing anything any more.
Separate booster-dev and kore-rpc-booster responses for collectiontest.k Separate kore-rpc-dev and kore-rpc-booster responses for test-vacuous Separate kore-rpc-dev and kore-rpc-booster responses for test-diamond Separate kore-rpc-dev and kore-rpc-booster responses for test-substitution Remove redundant booster-dev responses for test-substitutions Update test-3934-smt Update test-issue3764-vacuous-branch Update output for test-log-simplify-json
0c92b66
to
9c07a05
Compare
2ad1c79
to
09d68bb
Compare
09d68bb
to
586589f
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, a few suggestions
(Left ApplyEquations.SideConditionFalse{}, _) -> do | ||
let tSort = externaliseSort $ sortOfPattern pat | ||
pure $ Right (addHeader $ KoreJson.KJBottom tSort) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
...another place where we should probably catch UndefinedTerm
and return KJBottom
...
(Left err, _) -> | ||
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should probably also catch UndefinedTerm
here... (but for now the endpoint anyway returns errors when it is unsure)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Was this file supposed to be renamed (to state-vacuous-not-rewritten
) instead of deleted?
We have the renamed/new response files but no state-
file for it
|
||
If `assume-state-defined` is set to `true`, the all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. | ||
The `assume-defined` flag defaults to `false`. The `assume-defined` flag has different meaning in Booster and Kore. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe add (which is generally assumed by
kore-rpc-booster)
after the last sentence?
The `assume-defined` flag defaults to `false`. The `assume-defined` flag has different meaning in Booster and Kore. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. | |
The `assume-defined` flag defaults to `false`. The `assume-defined` flag has different meaning in `kore-rpc-booster` and `kore-rpc`. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules (which is generally assumed by `kore-rpc-booster`). |
Fixes #4012
Subsumes #4013 and #4011
Summary of changes:
"simplify"
endpoint in Booster, when given a pattern (term and predicate) now checks the predicate for SAT before attempting to evaluate the term, returning#Bottom
if the constraints are UNSAT."execute"
endpoint in Booster will now too check the constraints of the initial pattern for SAT before starting the rewriting loop. This initial check can be disabled by setting the execute request parameter"assume-defined"
tofalse
kore-rpc-booster
server will now effectively have--no-post-exec-simplify
option enabled as default, i.e. no simplification will be done at the Proxy level. The old behavior can be recovered by passing--post-exec-simplify
tokore-rpc-booster