[chore] stabilise SMT and bump provers

[fdupress]

@EasyCrypt/developers I need quick eyes on this, and for you to tell me how much of a pain in the arse it is to bump z3 to 4.16 and cvc5 to 1.1.x as a requirement for easycrypt dev.

I use arch (btw), so my own setup can follow SMT solvers relatively closely, but I recognise that not everybody likes to spend their weekend fixing their bootloader...

As a side note, most of the proof breakage is in places where the solver would need to recall that witness exists in all types, and to instantiate a universal quantification with it for the sake of a proof. I assume that both z3 and cvc5 have made a move towards more "constructive-compatible" heuristics in places, as they work to better integrate with ITPs.

[namasikanam]

As a side note, most of the proof breakage is in places where the solver would need to recall that witness exists in all types, and to instantiate a universal quantification with it for the sake of a proof. I assume that both z3 and cvc5 have made a move towards more "constructive-compatible" heuristics in places, as they work to better integrate with ITPs.

Just for my understanding, upgrading z3 and cvc5 makes their capability worse on dealing with witness?

[fdupress]

One of our two provers is such that the version we used in CI before this PR had no issue proving "(forall x, A x) => (forall x, A x => B) => B" whereas its new version stalls on it, or at least on instances of it that requires pulling witness out of a hat because there is no other x in context.

I won't try and speculate as to why this prover lost that capability. I will simply note in passing that the formula above is true only if types cannot be empty.

[fdupress]

A note on the current HEAD (reducing the timeout in all runs to 1): I ran this locally with a timeout of .5 and got two failing SMT applications that I could not reproduce consistently.

I am really trying to make this fail in the hope to identify all "bad places".

A note on the earlier discussion: it could well be that the regression on "goals whose proof require pulling witness out of a hat" is simply due to the fact that Z3 4.16 and CVC5 1.1 do not have bespoke Why3 drivers, rather than anything more problematic. But being stable without prover-specific optimisations seems like an OK goal to aim for, so I'll keep those changes even if we move back down to a supported version.

[fdupress]

First CI success with a 1s timeout!

Things to figure out:

• Is this consistent enough that we are happy to trust a 3s timeout in CI? 10s?
• Why is CVC5@1.3 not working when the docker image has CVC5 1.3.2 installed and recognised by Why3?

If the first question could be answered in review that would be great.

[fdupress]

• Why is CVC5@1.3 not working when the docker image has CVC5 1.3.[4] installed and recognised by Why3?

Explanation: why3.conf contains:

[partial_prover]
name = "CVC5"
path = "/usr/local/bin/cvc5-1.3.4"
version = ""

This is a why3/cvc5 bug, I think. I can reproduce it this outside of the docker container. The cvc5 1.3.4 release reports the following on cvc5 --version: cvc5 1.3.4 [git f3b21c4 on branch HEAD]
The cvc5 1.3.0 release reports the following instead: This is cvc5 version 1.3.0 [git tag 1.3.0 branch HEAD].

[fdupress]

Decision to merge this with Z3 4.16 and CVC5 1.1, 3 second timeout in CI.

[fdupress]

@strub quick review, please?

[vbgl]

FTR, I do observe some SMT instability there (last smt call on that line sometimes exceeds the timeout, z3 4.16.0):

[✗] examples/UC/dh_enc.ec: examples/UC/dh_enc.ec: line 1794 (35-36) cannot prove goal (strict)

[fdupress]

Thanks, @vbgl . Is that in CI, and is CVC5 set up as well?

I'll iterate on it, but really could not trigger failures with much smaller timeouts either locally (0.01s), locally in docker (0.01s), or in CI (1s).

[vbgl]

Yes, in CI. More configuration details:

known provers: CVC4@1.8.0, CVC4[counterexamples]@1.8.0, CVC4[strings]@1.8.0, CVC4[strings+counterexamples]@1.8.0, CVC5@1.3.2, CVC5[counterexamples]@1.3.2, CVC5[strings]@1.3.2, CVC5[strings+counterexamples]@1.3.2, Z3@4.16.0, Z3[counterexamples]@4.16.0, Z3[noBV]@4.16.0