[SMTChecker] Improve usability

[leonardoalt]

The SMTChecker's usability is still not great, especially for new users. When running the SMTChecker on large contracts with the default settings, users are often bombarded with warnings about targets the solver couldn't prove, and verifying all contracts at the same time makes the encoding very large. A few items that could be improved:

• [x] There is a lot of noise about targets that the solver could not prove. One idea is to compress all of those into a single warning by default, saying 128 verification conditions could not be proved. Consider choosing a single contract to be verified. To see the full list of unproved targets, enable model checker verbosity to 2 for example. This would also highlight problems that are actually confirmed.
• [x] Underflow/overflow verification conditions create A LOT of targets which really bloats the solver. IMO, these should not be checked by default for Solidity >=0.8.0 since most people do rely on the compiler's built-in checks. Conclusion, I think we should not check for underflow/overflow by default for Solidity >=0.8.0.
• [ ] Choosing a single contract to be verified increases performance a lot. Somehow deciding on a single contract (or a few) by default could also improve usability a lot.
• [x] Filter unsupported warnings by target contract reachability https://github.com/ethereum/solidity/issues/11703

[dtopia-me]

Hey there, not sure if this is the right place to raise this up, but throughout the whole Solidity document, neither definition, explanation nor the full name of SMTChecker is given anywhere. As you mentioned, not friendly for new users. It would be great if some background of this module or tool can be explained a bit further. Thanks.

[cameel]

@DeMeForYou It's there: SMTChecker and Formal Verification. It has been extended and made a top-level section only recently though so make sure you're reading the latest docs. Before then it was buried inside Security Considerations section.

[dtopia-me]

@cameel Thanks for this. What I meant was the fact that SMT stands for Satisfiability Modulo Theories is completely hidden in the current doc (I checked the entire doc and did not find what it stands for). New users and those who are not familiar with the term can google it for more details if the full name can be given.

[cameel]

There's a link to a Wikipedia article about SMT:

Solidity implements a formal verification approach based on SMT and Horn solving. The SMTChecker module automatically tries to prove that the code satisfies the specification given by require and assert statements.

But fair enough, it's not stated explicitly :) Perhaps we could expand on it a bit more. Would you be willing to submit a small PR to improve that part? The source is in https://github.com/ethereum/solidity/blob/develop/docs/smtchecker.rst.

[leonardoalt]

The name itself has a link to what it means. Sure making the full name explicit would explain strictly more than now, but does it really help more than giving an explicit link?

[leonardoalt]

Furthermore, how does saying that it's based on Horn solving also help a new user? Yes it needs to be said for completeness and for the more curious user, but it doesn't do anything in terms of usability.

[dtopia-me]

@cameel @leonardoalt Hey, thanks for the questions and comments. I'm speaking more from a consumer's perspective and that is indeed the experience I personally went through, which is 1) wondering what SMT is; 2) googling it for answers and got a bunch of solidity SMTChecker articles with no full name; 3) ah, found one link about Satisfiability Modulo Theories, but not sure if it is the one; 4) going through more links and found no direct answer. I think by having a full name explicitly displayed on the doc, readers can have the certainty that SMT is Satisfiability Modulo Theories, since new users do not necessarily have the knowledge to make the judgement.

It's good to know SMT is linked to a wiki page, and I have to say only until this moment did I know it is linked to the wiki page I found by googling. Besides, I've been reading the solidity doc in pdf on my pad, so clicking on it is just somehow infeasible.

[cameel]

Looks like there's now a separate issue for updating the docs (#11612) so let's move the discussion there and focus on the usability issues mentioned in the description here.

[chriseth]

I think all three items are very good suggestions. What are the exact open questions regarding those?

[leonardoalt]

I think all three items are very good suggestions. What are the exact open questions regarding those?

Acceptance.