Abstraction Refinement For Keccak

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.

The issue names no files, tests, or entry points. Begin by tracing where Keccak output constraints are added, then compare the fully abstract and concretized approaches against the performance and soundness requirements described here.

Written by the indexing model from the issue text.