halmos should not generate private keys that correspond to deployed contract addresses

[0xkarmacoma]

re: igorganich/damn-vulnerable-defi-halmos#3

imagine a contract deployed at address x, halmos can come up with a counterexample with a message signed by private key y, such that vm.addr(y) = x

basically we need to add a constraint saying that there is no private key that matches a deployed contract address

Taking note of a good stopgap measure proposed by @daejunpark:

we currently assume hash images are non-zero, but i was thinking to also assume they are large enough, say, greater than 2**64. indeed, we already assume they are small enough, less than 2**256 - 2**64. would this help? i mean, our create/create2-deployed addresses are 0xaaaaNNNN or 0xbbbbNNNN, which are smaller than 2**64

pros: super simple and efficient because we only add O(1) constraints
cons: would not work for etched contracts at hardcoded addresses

👍 probably a good tradeoff for now