Static Linux and Windows builds with Z3

[cameel]

The issue was raised in https://github.com/ethereum/solidity/issues/10166#issuecomment-734369933. I'm creating a separate issue to have a separate place to discuss it.

Currently some of our release builds are statically linked with Z3 (emscripten, macOS), some have SMTChecker disabled (Linux) ~and some are dynamically linked with it (Windows)~ EDIT: Windows build is a static one without Z3 too.

The main argument against statically linking Z3 is the increased binary size. The argument for it is that we're already doing it on some platforms and that having to jump through hoops to enable SMTChecker discourages people from using it.

Also, if we want it, should we rebuild older versions in solc-bin or is it enough to provide it in newer builds? We did include Z3 in rebuilds of older macOS and emscripten versions but since SMTChecker is still experimental, it might be fine to just add Z3 now and not worry about older binaries.

[d-xo]

Would be great to have SMTChecker enabled for linux static builds. I personally would also be happy to see it included in older versions (at least back until 0.6 or so maybe).

Do you know roughly the impact on binary size from including z3?

[cameel]

I think it should be comparable with the difference in macOS builds. See https://github.com/ethereum/solc-bin/pull/54#issuecomment-699991587. The size jumped from 4.6 MB in 0.4.16 (which was the last version before SMT) to 24 MB in 0.4.17. The latest binary is 32 MB, mostly due to solc itself.

The binary with Z3 is not huge in absolute terms but it's a big relative difference and multiplied by the number of platforms and versions, it matters in some contexts. For example the inclusion of Z3 in emscripten nightlies is the main reason why we went over the 10 GB limit in Github Pages so quickly and had to switch to a different way of hosting them. We're also not that far from going over the disk space limit in Github Actions (I think it's somewhere around 15 GB) which means that the CI workflows in solc-bin are going to become a little more complex - we won't be able to have a full checkout of the repo. We can handle the increase but we want to know it will actually benefit people and not be just dead weight.

[cameel]

We discussed it on the call today but haven't come to a decision yet:

• There was a proposal from @chriseth to provide two different release binaries for Linux. One with and the other without Z3.
• Currently the binary is completely static. We'd like to also provide a binary that can just dynamically link to system Z3 if available.
• @axic proposed two different builds: a size optimized one (with -Os and without static Z3) for use cases where it matters and speed optimized one (with Z3) for others.
  • Problem: Z3 is huge and probably won't be affected much by -Os anyway (we haven't tried though).
• One of the reasons why we still want to have a version without Z3 available is that when someone wants to just quickly try out several compiler versions, downloading big binaries is a pain.
• The conclusion for now was that we still need more feedback about use cases.

[d-xo]

@cameel thanks for all the info! :sparkles: :pray:

To make our use case clear: We have recently switched to using the static solc builds in dapptools, meaning that for recent versions of solc (0.7.x onwards) our linux users have no way to make use of the SMT checker with the solc versions provided by dapptools.

We believe that the SMT checker is a powerful and useful tool, and it is something that we ourselves use on audits, so we would very much like to be able to make this functionality available via dapptools without the hassle of maintaining our own CI chain specifically for solc (as we have been doing until recently).

[github-actions[bot]]

This issue has been marked as stale due to inactivity for the last 90 days. It will be automatically closed in 7 days.

[github-actions[bot]]

Hi everyone! This issue has been automatically closed due to inactivity. If you think this issue is still relevant in the latest Solidity version and you have something to contribute, feel free to reopen. However, unless the issue is a concrete proposal that can be implemented, we recommend starting a language discussion on the forum instead.