Keccak improvements

[msooseth]

Description

This change pushes the Keccak concretization to the very END of the steps we do. We don't concretize keccak (i.e. execute SHA3) during interpretation unless necessary (e.g. to do an RPC call). This allows us to take advantage of the fancy pattern matching in readStorage more often, hence making it more effective. In particular, this for example passes the new transfer-dapp test instantly that previously Z3 struggled with.

This improvement required quite a bit of change in the way we handle Keccak. The most hairy parts are:

• We now have a symbolic value in our VMOpts to know if we are doing concrete or symbolic execution. Concrete exe
• Keccak.hs now requires a bit more care, as we need to do some concretization as well
• we now have concKeccakSimp True/False to BOTH concretize and simplify (or not) the expression. This is basically a beefed-up simplify. This is sometimes needed, rather than pure simplify.
• in EVM.hs the accessStorage function had to be changed slightly so we can check whether we get a Nothing either with or without concretization. If we get a Nothing with either of the two, we do an rpc call. This is necessary, or we would never look up the rpc.

I also added a more thorough Add+Sub simplification. This is more complete than what we had. It was needed for one of the debugging sessions I was doing and so while it's unrelated, I think it should be OK(?) Let me know if you need it separately :)

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[msooseth]

OK, I think I managed to improve this a bit :)

[msooseth]

NOTE: I now know why we can't concretize earlier -- we could miss information that Keccak assumptions need. We COULD concretize earlier, but then the Keccak info would need to be extracted before concretization and passed to assertProps. Maybe it's worth thinking about. Right now it's "fragile" -- if we concretize earlier than assertProps, it can give spurious counterexamples.

[d-xo]

just one more small nit, but apart from that lgtm :)