Strengthen preconditions on polyveck_add() and polyvecl_add()

[rod-chapman]

Adds explicit bounds constraints on the inputs to these two functions. These significantly reduce the state space of the inputs, and therefore reduce the space that CBMC/Z3 has to search to find a proof.

Calling functions (attempt_signature_generataion() and crypto_sign_keypair_internal() ) re-prove OK with
these pre-conditions in place.

Proof times on macOS (before this PR) from main, for each parameter set:

polyveck_add: 31s,56s,63s
polyvecl_add: 30s,66s,65s

Proof times after this PR:

polyveck_add: 20s,36s,40s
polyvecl_add: 22s,31s,22s

[mkannwischer]

Thanks @rod-chapman.

I think the pre-conditions can be simplified unless I am missing something.

[rod-chapman]

New proof numbers for MLDSA-87 on my Mac, following removal of the redundant preconditions, plus proofs of the 2 calling functions:

| Proof                            | Status  | Duration (in s) |
|----------------------------------|---------|-----------------|
| crypto_sign_keypair_internal     | Success | 34              |
| mld_attempt_signature_generation | Success | 121             |
| polyveck_add                     | Success | 18              |
| polyvecl_add                     | Success | 18              |

[mkannwischer]

Apologies for not noticing this earlier, but I belive the functional post-condition is no longer needed after #637.
That could further improve proof time.

Maybe the poly_add() contract can be adjusted accordingly (not sure about this part).

[rod-chapman]

The post-condition and loop invariant of polyvecl_add() can be weakened as you suggest.

The same for polyveck_add() cannot be done, since the stronger post-condition is required to prove crypto_sign_keypair_internal()

I will commit and push now.

[mkannwischer]

The post-condition and loop invariant of polyvecl_add() can be weakened as you suggest.

The same for polyveck_add() cannot be done, since the stronger post-condition is required to prove crypto_sign_keypair_internal()

I can't follow. In crypto_sign_keypair_internal(), the output of polyveck_add() is consumed by mld_polyveck_reduce whose precondition is

  requires(forall(k0, 0, MLDSA_K,
    array_bound(v->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))

So this should work.

Now I notice however, that the post-condition of polyveck_add is currently

  ensures(forall(q2, 0, MLDSA_L,
                array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))

this should be

  ensures(forall(q2, 0, MLDSA_K,
                array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))

With that fix it proves fine for me without the additional post-condition.

[rod-chapman]

Aha! Well spotted! I will fix as soon as I have a moment...

[rod-chapman]

Corrected. Proof times for MLDSA87 on my Mac:

| Proof                            | Status  | Duration (in s) |
|----------------------------------|---------|-----------------|
| crypto_sign_keypair_internal     | Success | 30              |
| mld_attempt_signature_generation | Success | 96              |
| polyveck_add                     | Success | 10              |
| polyvecl_add                     | Success | 8               |

[rod-chapman]

CI looks good.

[mkannwischer]

Thanks @rod-chapman. LGTM. Please clean-up the commit history then this is good to merge.

[mkannwischer]

LGTM. Thanks @rod-chapman!