search

runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
BSD 3-Clause "New" or "Revised" License
506 stars 140 forks source link

Removing `#rangeBool` reasoning #2616

Closed PetarMax closed 3 weeks ago

PetarMax commented 3 weeks ago

The lemmas removed in this PR slow down execution of some real-world proofs considerably because the rangeBool constraints are SMT-checked for every expression of the form notBool ( X ==Int 0 ) or notBool ( X ==Int 1 ).

The lemmas brought in reflect the (so-far-observed) checks made by the compiler, and their LHS is complex enough so they it will not be matched against unnecessarily.

PetarMax commented 3 weeks ago

(Some of) the added lemmas are tested by some of the dsvalue tests in the mcd and mcd-structured test suites, via the compiler-introduced checks.

I am not sure what a reasonable test that is not direct would look like.