CBMC: Improve proof stability #611
Conversation
Signed-off-by: Matthias J. Kannwischer <[email protected]>
Signed-off-by: Matthias J. Kannwischer <[email protected]>
1. Weaken post-condition and loop invariant in polyvecl_add(). The stonger post-condition was unncessary. 2. Simplify polyvec_matrix_expand(). Small performance loss here since batched_seeds[] is (re-) initialized every time. This is bit slower but removes a loop statement entirely. 3. Refactor polyvec_pointwise_acc_montgomery() by splitting core "sum of products" calculation into a distinct local function mld_pointwise_sum_of_products(). Add proof of the latter. Proof time for parameter set 87 now 4 minutes (real-time) and 40 minutes (user time) with 64 cores on an r7g instance. Signed-off-by: Rod Chapman <[email protected]>
1. Weaken the contract of mld_polyveck_add(). This is sufficient to prove the caller in mld_attempt_signature_generation() 2. Introduce a new mld_polyveck_add_error() with stronger contracts where the second argument is an error term where all coefficients are bounded in absolute value to MLDSA_ETA. The post-condition of this function is just right to prove the calling code in crypto_sign_keypair_internal() which relies on these stronger bounds. 3. Add proof artefacts as appropriate. Signed-off-by: Rod Chapman <[email protected]>
Signed-off-by: Rod Chapman <[email protected]>
| #ifndef CBMC | ||
| for (i = 0; i < MLDSA_K; i++) | ||
| { | ||
| for (j = 0; j < MLDSA_L; j++) | ||
| { | ||
| mld_poly_permute_bitrev_to_custom(mat[i].vec[j].coeffs); | ||
| } | ||
| } | ||
| #endif /* !CBMC */ |
There was a problem hiding this comment.
I think this is a very bad idea. (1) It introduces a proof gap; (2). It's ugly.
There was a problem hiding this comment.
I agree! Unrolling the loop leads to instability, so I will see if I can do it with an invariant.
There was a problem hiding this comment.
or factor it out into a distinct function.
There was a problem hiding this comment.
Factoring it out would also align it with mlkem-native - I'm in favour of that! Thanks.
There was a problem hiding this comment.
Data:
Proof times for the 3 parameter sets as-is on r7g: 25s, 2m38s, 4m respectively.
With the #ifndef CBMC guard removed, it's 30s, 100s, and "gave up after 30 minutes".
Refactoring into a single function as-per mlkem-native looks like the best option.
|
Proof runtime in CI improves significantly:
More importantly: It makes proofs in #558 feasible. |
This hoists @rod-chapman's work to fix and stabilize CBMC proofs in #558.
The changes are independent of the changes in #558, so we should review and merge them separately.