[Haskell-Performance] kevm proof slow with extra side conditions

Please Prepare Test Data

I have a specification on KEVM: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/benchmarks/storagevar03-spec.k

This can be run with: make tests/specs/benchmarks/storagevar03-spec.k.prove after building KEVM.

It has some side-conditions for validity on the input state: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/benchmarks/storagevar03-spec.k#L116. But these side-conditions are actually not needed (the lines CONTRACT_ID >Int 0 andBool notBool #isPrecompiledAccount(CONTRACT_ID, BYZANTIUM)), so I removed them.

Removing these 4 conditions (on CONTRACT_ID and CALLEE_ID) ends up improving the performance by ~2.5X.

So it seems that having these extra side-conditions is causing a big performance slowdown.

I've attached 2 bug reports:

• kevm-bug-storagevar03-with-conditions.tar.gz, which is run with the extra conditions as linked above, which takes 269.4s on my machine.
• kevm-bug-storagevar03-without-conditions.tar.gz which is run with those conditions removed and takes 117.31s my machine.

These conditions should not change their simplification status through the whole proof beyond startup, so I guess I'm wondering why it takes so much longer to run with these extra conditions. We should try evaluating them once, and then basically know that they can't be simplified any further throughout the rest of execution (so should not try).

Start with tests/specs/benchmarks/storagevar03-spec.k and run make tests/specs/benchmarks/storagevar03-spec.k.prove after building KEVM. Compare the attached bug reports with and without the four side conditions, focusing on why simplification continues to impose a cost. Done when the performance difference is explained and the relevant behavior is corrected or documented with a regression check.