`STATICCALL` (and later `EXTCODESIZE` & `CALL`) overapproximation needs *much* better explanation

[msooseth]

We have a new system that overapproximates in certain cases. However, it turns out that this can be confusing to users.

If the address is fully symbolic, e.g. fun(address myaddr) and later this stuff is called, we overapproximate and return some nonsense value for myaddr -- because it hallucinated that the contract at that address e.g. returned abba in the returndata. In this case, the SMTCex will contain staticall-result-data-0 set to ConcreteBuf "abba". But the system needs a solution to the address myaddr in order to generate a SMTCex, so it will come up with some value for the address myaddr that doesn't make any sense. The definition of that contract is simply that for the value it is called with (whatever it was) it returns aabb.

This definitely needs documentation at https://hevm.dev And it needs to be explained to the user during the counterexample generation so they are not surprised and start looking for a contract at that nonsense address. In fact, the address should not be shown, instead, we should tell the user that at that symbolic address, the contract must put aabb in the returndata.

[msooseth]

For example:

Sat (SMTCex {vars = fromList [
(Var "staticcall-result-stack-0" 0x1)]
 addrs = fromList [(SymAddr "arg1" 0x13FBd0351503fBeA7A59A6aD2D65b9Ec61435a5C)]
 buffers = fromList [(AbstractBuf "STATICCALL-result-data-0" Flat "") (AbstractBuf "txdata" Flat "")]
 store = fromList []
 blockContext = fromList []
 txContext = fromList [(TxValue 0x0)
]})


Sat (SMTCex {vars = fromList [
(Var "staticcall-result-stack-0" 0x0)]
 addrs = fromList [(SymAddr "arg1" 0x13FbD0351503Fbea7A59a6AD2d65B9ec61435a5C)]
 buffers = fromList [(AbstractBuf "txdata" Flat "")]
 store = fromList []
 blockContext = fromList []
 txContext = fromList [(TxValue 0x0)
]})

Notice that in the first case, the staticcall was successful and returned an empty returndata. In the scond case, it was not successful, with a 0x0 returnvalue and the returndata was not used/checked (hence no value for it).

This should be explained to the user.