Some bitwise and bool2Word lemmas

[ehildenb]

This PR is the first of several that will come from some experiments with the Kontrol test-suite. This one adjusts the semantics and lemmas, in particular:

• In the process of exploring generated claims from Kontrol test-suite, several simplifications were revealed that seem generally useful. The simplifications are added along with tests:
  • A rule about simplifying X xorInt Y <Int 0 -Int X, if X and Y are both positive.
  • Rules about simplifying X ==Int 0 when disequalities about X around zero are known.
  • Claims which were failing before and now are passing with these lemmas are added.

[PetarMax]

Lemmas like these tend to slow down the execution. @dwightguth has flagged this in the Maude backend, I've also noticed a considerable speedup once I commented slightly more general lemmas that we had out of the work on symbolic calldata. The CI is currently timing out and lasting almost double the time it did before.

I remember introducing these more general lemmas for Optimism because of the looping on the symbolic size of a bytes parameter, getting constraints of the form 37 <=Int X and X <=Int 37, and the backend not understanding without SMT that X ==Int 37. The lemmas were:

rule   A <=Int B                =>   A  ==Int  B   requires B <=Int A [simplification, concrete(A)]
rule { A <=Int B #Equals true } => { A #Equals B } requires B <=Int A [simplification, concrete(A)]
rule { true #Equals A <=Int B } => { A #Equals B } requires B <=Int A [simplification, concrete(A)]

How did these two lemmas come up?

[ehildenb]

The tests added are exactly the expressions that came up causing these lemmas to be added. I can try out the lemmas you suggest.

Whenever I run into something unsimplified that I want simplified, the first thing I do is snip out that expression and add it as a test to KEVM. Then I begin working on that test directly.

[PetarMax]

Yes, I understand that. I'm not suggesting that you replace your lemmas with the ones I suggest. All that I am saying is that I had similar lemmas that were slowing down the performance. I suspect that your lemmas are causing a slowdown that resulted in the CI failure. Have you got a performance comparison of this branch vs master?

[PetarMax]

I think that we could benefit from introducing simplifications that only do a syntactic search of the pure constraints. For example:

rule X ==Int 0 => true requires 0 <=Int X andBool X <=Int 0 [simplification, comm, syntactic]

would only fire if the requires clause conjucts were verbatim in the pure constraints. I think this is the case in the examples that motivated this particular simplification and I know it was the case when I introduced the more general ones.

[ehildenb]

It appears that all proofs take the same amount of time as master, except the bihu functional specification here, which loops:

evm-semantics/tests/specs/bihu/functional-spec.k

Line 18 in dca9426

claim <k> runLemma(#range( _MEM [ 96 := #padToWidth(32, #asByteStack(BS)) ], 96, 32))

.

I'm investigating.

[yale-vinson]

Any update on this one? I see from two weeks ago you are investigating, but curious to see if you made any headway on it?

[ehildenb]

Subsumed: #2270
Subsumed: #2253