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
Generalising bitwise simplifications #2251
Conversation
Can you post performance numbers for the entire KEVM test-suite and the Kontrol test-suite please (comparing this branch to master). I suspect this may have a slowdown in some cases. |
Running the entire test suite locally for me is complicated. I will wait to see the CI numbers first. |
There are instructions here for KEVM: runtimeverification/hs-backend-booster#355. Note that these instructions are for comparing booster to legacy backend, but you should compare booster on master vs booster on this branch. Similar instructions work for Kontrol. |
These is the performance comparison for KEVM on all tests, it does not appear to be statistically significant overall, with the PR times being slightly faster than the master times:
This is likely because the booster can easily discharge the concrete
the first, second, and third condition are all fully concrete always. |
kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
Outdated
Show resolved
Hide resolved
kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
Outdated
Show resolved
Hide resolved
kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
Outdated
Show resolved
Hide resolved
…ification.k Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
Show resolved
Hide resolved
Just to note, I've noticed a substantial difference in the times when running the test suite with eight parallel processes and with one. Below are the results with
|
This PR generalises several lemmas on bitwise operators, streamlining the development.
The corresponding tests are already present.