Abstraction Refinement For Keccak

[d-xo]

Right now we eagerly add a lot of complex and expensive constraints on the output of keccak (injectivity, large gaps, no collisons with value type storage slots). These are not always needed, and can significantly impact performance (e.g. adding large gaps slowed our test suite down a lot). In addition, these constraints may not even be precise enough since the solver will always produce a model for keccak that diverges from the real implementation.

We should consider the following:

1. Add the constraints on keccak only if needed (i.e. if we get sat with a fully abstract model)
2. Consider concretizing keccak outputs in a bottom up fashion (i.e. get a model from the solver for the deepest input, and then iteratively add constraints that the keccak outputs match the outputs of the real function on the concretized inputs). This is not a sound refinement in general (turning something sat into unsat with this approach does not imply safety), but if we remain sat, then the model we return will be correct.