search

awslabs / LibMLKEM

Apache License 2.0
15 stars 1 forks source link

Upgrade from cvc4 to cvc5 #3

Open UlysseDurand opened 3 months ago

UlysseDurand commented 3 months ago

This makes reference to the issue https://github.com/awslabs/LibMLKEM/issues/1.

I made gnatprove use cvc5 and added one Assert to make it prove everything (with my computer, cvc5 failed to prove the assertion line 1614).

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

rod-chapman commented 3 months ago

Please tell me exactly which version of CVC5 you are running, and I will try to reproduce results here. Earlier versions of CVC5 were worse than CVC4, particularly in Bit-Vector reasoning. This was acknowledged by Andrew R, Clark and the other CVC5 developers some time ago, but I was waiting for it to get fixed before committing to the switch.

UlysseDurand commented 3 months ago

My version of CVC5 is 1.0.5, it completed all the proofs on my side but I understand it might be less efficient on some operations.

rod-chapman commented 3 months ago

I am building CVC5 1.1.2 here on macOS to see what I get. I will post results soon.

rod-chapman commented 3 months ago

OK... with Z3 4.12.5, CVC5 1.1.2 and AltErgo 2.4.0, all proofs are OK with no change to the sources at all.

With CVC5 1.1.2 ALONE, I see 29 undischarged VCs, so still room for improvement there...

rod-chapman commented 3 months ago

With CVC4 1.8 ALONE, I get 21 undischarged VCs, so CVC5 is still worse in some areas...

yannickmoy commented 3 months ago

@rod-chapman don't you want to upgrade to cvc5 in that case? CVC4 is not maintained, and bugs could be present, with no guarantee that they would be fixed.

rod-chapman commented 3 months ago

As of now, I am happy to upgrade, since CVC5+Z3+AltErgo is equal in performance to CVC4+Z3+AltErgo. In the long run, I want CVC5 to prove the whole library on its own. To that end, I am trying to submit the LibMLKEM SMT files as a benchmark for future runs of SMT-Comp.