Z3 version upgrade

[mtzguido]

Hi F* hackers,

We are currently working on upgrading the Z3 version that F* uses from 4.8.5 (released in 2019) to the latest master, which would probably be 4.12.3 once released.

Thanks to a lot of help from Nikolaj Bjørner, the impact is actually rather minor. With his fixes, the files that need tweaks across our everest projects are close to none! For example here's the full diffstat for HACL*.

 code/chacha20/Hacl.Spec.Chacha20.Equiv.fst         |  3 +-
 code/k256/Hacl.Impl.K256.Verify.fst                |  1 +
 code/sha2-mb/Hacl.Spec.SHA2.Equiv.fst              |  6 +-
 code/sha2-mb/Hacl.Spec.SHA2.Lemmas.fst             | 11 +++-
 code/streaming/Hacl.Streaming.Functor.fst          |  4 +-
 lib/Lib.Buffer.fst                                 |  2 +-
 vale/code/arch/Vale.Arch.BufferFriend.fst          | 11 +++-
 vale/code/arch/x64/Vale.X64.Lemmas.fst             | 17 ++++--
 .../poly1305/x64/Vale.Poly1305.Bitvectors.fst      |  2 +-
 .../x64/Vale.Poly1305.CallingFromLowStar.fst       |  4 ++
 ...Vale.Transformers.BoundedInstructionEffects.fst | 64 +++++++++++++++++-----
 11 files changed, 93 insertions(+), 32 deletions(-)

Some of it are just generic robustness improvements. The last file I reworked quite a bit to reduce the rlimit from 400 to 40. I still have one admit (which I think it's due to a Z3 regression), and a patch to Z3 that I need to run by Nikolaj, but otherwise the new Z3 already works.

So, given that we are very close, we could start syncing as to how to make the upgrade happen. Especially across projects, without having to do so atomically.

Here's some ideas:

0. First, note that F*'s SMT encoding is not heavily tied to the Z3 version-- it's just SMT2 (otherwise we'd be toast)
1. For the new version, F* just needs to give some (new) options to Z3. So, we will add a way for F* to detect which Z3 version it is talking to and choose the relevant set of options for it.
2. We would add a new ''--z3version" option to tell F* which Z3 version it should use. The default would be (for now) "4.8.5", but projects could downgrade/upgrade it, even via #push-options for individual definitions.
3. F* will look for z3-VERSION (e.g. z3-4.8.5, with an .exe suffix in windows) in the PATH, to enable transparently switching versions within a single machine.
4. If z3-VERSION is not found, F* will try just z3, and warn if the version is not the expected one (as it does now). This is only for compatibility, ideally, I think versions would always be explicit in the filename.
   • Perhaps F* can also look in its home for Z3, instead of relying on the PATH.
5. Use of the --smt option overrides all of the above, F* will use exactly that executable, and warn on a mismatch.
6. Doing that, I think we could just install z3-4.8.5 and z3-4.12.3 in our PATHs, and in the CI images, and then choose versions for each particular project using the version flag.
   • We could kind of​ do this already with the --smt flag, but
     • we still need point (1) above
     • it would not be possible to change versions within a file (--smt is disabled for pragmas, mostly for security reasons)
     • that would rely on Makefile support with OTHERFLAGS.
7. When convenient, we flip the default from 4.8.5 to 4.12.3.

My main questions are:

1. Do you think this version option and switching makes sense?
   • Would it be comfortable for your local hacking?
   • Does it work well for your CI systems (and Nix)?
2. Note that installing z3 via opam would not be very convenient now: the executable is just named "z3" (though maybe there's a switch to change it? I don't know), and we can only install one given version.
   • We should just use the FStarLang/binaries repo to hold all of the versions we care about, or just fetch them from Z3 releases
   • I think this is actually an improvement regardless of this upgrade, since opam builds Z3 from source, and that takes over 1 CPU-hour.
   • Also I think we can just host/download the Z3 binary, no need for the include directory, dynamic library, etc.
3. I will add support for all these options to F* before actually flipping the default version. I'll make a PR for that and we could discuss there too.
4. Going forward, we plan to have a nightly Z3 job that tests against the current Z3 master branch, to make future upgrades easier, and to serve as a regression test for Z3 itself.

Once I get a full everest green with the new Z3, I'll run a detailed performance comparison and post it here. Unscientifically, I haven't observed a performance degradation, but I've indeed observed some improvements.

Guido

[TWal]

Incredible!
After chatting with Nix folks at Inria, our CI should handle this with no problem (especially with the backward compat solution you propose).
Thank you for this work :)

[cmovcc]

Hi! I mentioned this discussion here: ocaml/opam-repository#24618, but discussions do not seem to add mentions in the same way as issues or pull requests. The opam z3 4.8.5 package currently depends on Python 2, which is now often unavailable (e.g. on Debian stable). This opam-repository PR fixes this by replacing Python 2 dependencies with Python 3 ones, so that if z3 4.8.5 is still used, it can be built seamlessly. Nothing related to the z3 version should break. This is just a heads-up, please tell me if somethings seems wrong. And by the way, thank you very much for this work, looking forward to see the z3 default version flipped! Edit: due to some version constraints that will likely be fixed, the opam CI does not mention F*, but it already passed the F* build test in a previous PR iteration.