[SMTChecker] Study Spacer's limits

[leonardoalt]

Collecting some samples here where Spacer fails to prove/refute something, to try to understand why.

• multisig https://gist.github.com/leonardoalt/66576430ca21d849dfdb138594c93d89 Here the assertion is proved, which is really good! It answers might happen for the possible overflow. My guess is that it fails at unrolling the overflow because it's a 1-increment and a cex would take 2**256 txs.

• erc777 https://gist.github.com/leonardoalt/bf22ba50585363e276395bb4b2d0553d A couple arithmetic might happen. The one related to totalSupply might be hard because it might need the invariant totalSupply = sum(balances). However I think the one related to balances shouldn't be too hard. If you uncomment the external calls it gets harder.

A few small but not necessarily simple examples from our own test suite: abi/abi_encode_with_selector_vs_sig.sol operators/compound_bitwise_or_uint_1.sol operators/slice_default_start.sol external_calls/external_inc.sol loops/for_1_fail.sol

[blishko]

Analysis of loops/for_1_fail.sol: This example is a relatively simple for loop where Spacer does not seem to be able to prove that increment insider the loop body does not overflow. This actually requires only integer reasoning and so Spacer should be able to deal with it. In fact, after Horn clauses produced by our encoding has been stripped off the unnecessary blockchain-related variables, Spacer immediately solved it.

Further investigation showed that the reason of divergence in this case are the transaction data. When that variable has been removed from the encoding, Spacer solved the problem. In fact, it is sufficient to remove only all constraints related to the transaction variable tx_0 and then Spacer probably figures out that it can slice the variable away and solves the problem.

This has been confirmed also directly: Changing the encoding so that SymbolicState::txConstraints returns smtutil::Expression(true) leads to successful proof that the overflow cannot happen in this example.

Running isoltest with disabled transaction constraints gave mixed results:

• In general, Spacer was able to produce more counter-examples in general. But also some examples where it actually got worse were seen.
• Nondeterminism in Spacer still plays a big role. When version pragma was added to the loops/for_1_fail.sol, Spacer diverged even without the transaction constraints. This might suggest that the nondeterminism, rather than the removed transaction constraints, was responsible for the successful solving.

[leonardoalt]

Over time we learned that our heavy use of ADTs was a problem for Spacer. This has been improved in the solver since then.