Use upstream instead of local version of z3 4.15.3

[nmouha]

Use the upstream instead of the local version of z3 4.15.3.

This avoids unnecessary compilation, because this version is present in Hydra's build cache.

[mkannwischer]

Thanks @nmouha - nice improvement saving time to setup.

One small suggestion.

[mkannwischer]

Please keep the z3.overrideAttrs - even with that nix will take it from the binary cache, but we do not risk unintentionally switching to a newer version when updating the unstable version.

[nmouha]

Thanks @mkannwischer for the quick feedback!

I changed my PR to keep z3.overrideAttrs as you suggested. Also, I've confirmed that nix will still use the binary cache.

It was actually my intention to switch to a new version of z3 whenever it's available. In the coming days, nixos-unstable will update z3 from 4.15.3 to 4.15.4. (The version update was merged to master yesterday, it takes a few days to move down.) It seems to be a lot of hassle to manually keep track of new versions of many dependencies, but of course it's okay if you want to do this.

My suggestion would be to add mlkem-native as a new package to Nixpkgs, starting by adding some of the missing packages that it depends on. This should decrease the maintenance burden: the Nixpkgs CI would flag if any proposed change to Nixpkgs master would break (failing build or tests) for mlkem-native or any its dependencies.

[mkannwischer]

Thanks @nmouha.

Some context: We had quite a few issues with proof performance regressions for various versions of z3. At first, we followed your approach of always updating to the latest version in nix-unstable, but eventually we ran into big issues with some larger proofs in mldsa-native that just wouldn't work with newer versions of z3 and we had to revert to 4.12.
It turned out that this was a known problem within the CBMC team, and since then we have been sticking to their recommendations.

Since 4.15.3 seems good again, maybe we can at some point switch to just taking whatever nix unstable gives us, but for now I'd rather not have the pain of debugging z3 performance again.

Note that z3 is the only dependency we do this for - for everything else we just take what ever nix gives us.

[nmouha]

Thank you, @mkannwischer, for the additional context!

It seems that some of the SMT queries generated by CBMC are experiencing performance regression even in z3 4.15.3 and z3 4.15.4 (Z3Prover/z3#7991). So, it makes sense to pin specific versions of z3 until the performance issue are sorted out.