Problem with reproducing the proofs

[UlysseDurand]

I had trouble reproducing all the proofs (most of them work) Launching gnatprove -Pmlkem -u src/mlkem.adb, it tells me there are 5 "Unproved".

Those are :

mlkem.adb:270:25: medium: assertion might fail
  270 |         pragma Assert (T (R) = T (X mod Q));
      |                        ^~~~~~~~~~~~~~~~~~

...

mlkem.adb:990:14: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove Bits_12_To_U16 (B (K * 12 .. K * 12 + 11)) < Q
  990 |             (Bits_12_To_U16 (B (K * 12 .. K * 12 + 11)) < Q));
      |             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

...

mlkem.adb:1614:22: medium: assertion might fail
 1614 |      pragma Assert (K = 128);
      |                     ^~~~~~~

...

mlkem.adb:1671:36: medium: loop invariant might fail in first iteration
 1671 |            pragma Loop_Invariant (I32 (K) = 2**I + Count - J - 1);
      |                                   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

...

mlkem.adb:1685:22: medium: assertion might fail
 1685 |      pragma Assert (K = 0);
      |                     ^~~~~

I am running Ubuntu and I followed the installation in the spark_ada/README.

There was a warning cvc4 is deprecated, changing to cvc5 in the file mlkem.gpr helped, now there is only one "Unproved", which is

mlkem.adb:1614:22: medium: assertion might fail
 1614 |      pragma Assert (K = 128);
      |                     ^~~~~~~

[yannickmoy]

Indeed, if Rod relied on CVC4 for proofs, and you did not install it, that explains the difference! Now that you're using cvc5, it also explains why you have one check in diff. I suggest you look at how to make this assertion proved with z3/cvc5/alt-ergo.