[SMTChecker] New default settings

[leonardoalt]

Depends on https://github.com/ethereum/solidity/issues/11703

Currently the default settings are still heavy enough that users don't really know if the smtchecker is doing something and it might take a long time until the users see anything. We already disabled overflow/underflow checks by default because those just create too many queries and give the impression it's stuck. However, as @cameel pointed out in https://github.com/ethereum/solidity/issues/11703, we could do more to make it lighter for the users.

@cameel suggested an explicit "light" mode where no "unsupported" warnings would be given, and fewer things would be checked. I think we should rather make the default mode light. So here's my suggestion for the default mode:

• Compressed "unproved targets" warning (already done, 1 warning for all unproved targets, user needs to explicitly say they want the full list)
• Compressed "unsupported Solidity feature" warning (https://github.com/ethereum/solidity/issues/11703)
• Use a low timeout instead of resource limit. Currently we use resource limit as the default to make queries deterministic for the tests. This is rather user unfriendly though. I think we should still have the tests use rlimit for determinism, but the default settings should be a low timeout of like 1s per query.

[PaulRBerg]

While we are at it, I want to also mention a related issue I opened in the Foundry repo:

https://github.com/foundry-rs/foundry/issues/3904

Now, I realize that that my Foundry feature request could be turned into a feature request for Solidity itself.

Copy-pasting what I said in the other thread:

The default Yul optimizer step sequence is quite long-winded - even in the Solidity source code, the default value is split on multiple lines for readability purposes.

My feature request is to make it possible to pass the default value to the optimizerSteps field in the Foundry config, so that users don't have to manually write it up:

[profile.default.optimizer_details.yulDetails]
stackAllocation = true
optimizerSteps = "default"

[leonardoalt]

Which sequence exactly do you mean by default?

[PaulRBerg]

This:

https://github.com/ethereum/solidity/blob/59f9ab4dee8da6ad12faa5ae6e7d46209e506544/libsolidity/interface/OptimiserSettings.h#L44-L60

[leonardoalt]

But that's already the default, so there's no need to give that to Foundry

[PaulRBerg]

Actually, there is a use case for this in sophisticated set-ups (ironically, set ups that you and I have previously discussed on Twitter):

This is useful because users may want to disable the default step sequence during development (i.e. in the default profile) in order to speed up the compilation time. But then, in a separate profile such as production, users may want to set the step sequence back to the default to get maximum optimization benefits.

[leonardoalt]

Yea, I agree with that. But I think that if you simply enable the optimizer in the other profile, without explicitly setting the steps, it should use the default steps, shouldn't it?

[PaulRBerg]

Nope - Foundry will fallback to the optimizer_details settings from the default profile. I don't have this set up handy now but I'm quite sure that this is the behavior that I noticed when I opened the Foundry issue.

[leonardoalt]

Ah ok, that clarifies it, thanks. I agree with the default value.

[cameel]

Nope - Foundry will fallback to the optimizer_details settings from the default profile.

This sounds to me like a problem on the Foundry side though. They could just not pass any value to the compiler when they detect the default.

On the compiler side, the way to specify the default currently is to omit the value (null might work as well in Standard JSON). I wouldn't be against having a way to specify that explicitly but unfortunately default is itself a valid sequence and we lack a good convention for that on the CLI and Standard JSON.

By the way, this is off-topic here so I'm going to mark the comments as such not to distract from main point of this issue, which is the light mode for SMTChecker :)

[leonardoalt]

This is currently stuck in a z3 timeout bug when running via soljson. I think we need to call it a day and go with "timeout is unsupported when using the static webassembly z3" and ship this.