CVC5 unable to reason about "power" function

[rod-chapman]

Dear AdaCore,
I'm experimenting with verification of some cryptographic code (in this case the LibMLKEM library). We have found that CVC5 1.2.0 is very poor at reasoning about the "power" theory for integers, and we have to fall back on AltErgo to discharge those VCs.

BUT... we find that CVC5 has a built-in "int.pow2" operator, which it is able to reason with. If I remove the "power" theory from the SMT file, and change all instances of (power 2 i) to (int.pow2 i) then CVC5 proves my VCs almost instantly. Perhaps gnatprove could be changed to use "int.pow2" where possible when --prover=cvc5 is selected?

This is using GNATProve 14.1.0 on macOS.

I can send example SMT files if you'd like to see an example.

[HuStmpHrrr]

Just to add a bit more information: z3 also support exponential natively. I can see that the definition and the properties of power are generated to regulate the model of power to make sure the model meets what we expect. I do not think that's necessary anymore with modern z3 and cvc5.

[kanigsson]

Hello Rod and Jason,

thanks for this investigation. I will bring this up with the Why3 team who is maintaining the prover drivers.

Johannes

[clairedross]

Hello,
Just to complement Johannes' answer, I wanted to add that even if some construct is supported in the underlying SMT solver, it does not mean that it is necessarily beneficial overall to use it. It generally depends how heavy the support is. More precisely, there are VCs where the construct occurs which would benefit from more precision, and others which do not need it, it is always like that. If the precise support is so heavy that it degrades the second kind of VCs too much, it can happen that it enabling this support is detrimental overall.
Best,

[rod-chapman]

Here's an example.

power.smt2 is a VC generated by SPARK Pro (line 1499 of mlkem.adb in the LibMLKEM repo). CVC5 1.2.0 is completely defeated by this.

pow2.smt2 is the same file, but replacing "(power 2 " by "(int.pow2 " in 4 places. CVC5 says "unsat" in about 0.04 seconds on my laptop.

It would be interesting to try this change on your entire test suite and see what happens...
power.smt2.gz
pow2.smt2.gz

[HuStmpHrrr]

Hi Claire,

I agree with everything you said. I think the best thing to do is to have options to choose different generated VCs, and let the application layers to worry about which version is the best for them. The current generated power is most definitely unhelpful for CVC5 (probably less so for Z3), because it is defined through a sequence of assertions. A better alternative is to define recursive functions (define-fun-rec), if a custom power function is needed. In any case, I think CVC5 in general is benefited from using builtin Int.pow and Int.pow2.

[kanigsson]

Hello Rod,

Could you please provide Ada code with which we could test this? It would help us validate our potential solutions.

[rod-chapman]

Look at the main branch of the LibMLKEM repo, and the function NTT that starts on around line 1466 of spark_ada/src/mlkem.adb

I generate VCs with gnatprove 14.1.0

gnatprove -Pmlkem --prover=cvc5 --debug -u src/mlkem.adb

Several examples in there of VCs involving "(power 2 x)" that CVC5 1.2.0 cannot solve.

[rod-chapman]

I also used this little Shell script

#!/bin/zsh
for I in *.smt2
do
   sed -i -e "s/(power 2 /(int.pow2 /g" $I
done

to change all instances of "(power 2 " to "(int.pow2 "

Do that to all the files, re-run CVC5 on all of them and see the difference!