CBMC: Identify long running CBMC proofs and study potential for speedups

[hanno-becker]

Some CBMC proofs take >10min, leading to long CI runtime (and associated cost).

Acceptance criterion:

• [ ] Identify which CBMC proofs are the most time consuming.

Bonus: Come up with concrete ways/ideas how to speed them up.

[hanno-becker]

357 shows what the big hitters are. For K=3:

  |.Proof                                 | Status  | Duration (in s) |
  |---------------------------------------|---------|-----------------|
  | barrett_reduce                        | Success | 4               |
  | basemul_cached                        | Success | 63              |
  | cmov_int16                            | Success | 2               |
  | fqmul                                 | Success | 11              |
  | gen_matrix_entry                      | Success | 125             |
  | montgomery_reduce                     | Success | 2               |
  | pack_pk                               | Success | 4               |
  | poly_add                              | Success | 3               |
  | poly_basemul_montgomery_cached        | Success | 291             |
  | poly_cbd_eta1                         | Success | 6               |
  | poly_cbd_eta2                         | Success | 3               |
  | poly_compress                         | Success | 3               |
  | poly_decompress                       | Success | 5               |
  | poly_frombytes                        | Success | 5               |
  | poly_getnoise_eta1122_4x              | Success | 3               |
  | poly_getnoise_eta1_4x                 | Success | 4               |
  | poly_getnoise_eta2                    | Success | 5               |
  | poly_getnoise_eta2_4x                 | Success | 5               |
  | poly_mulcache_compute                 | Success | 4               |
  | poly_reduce                           | Success | 4               |
  | poly_sub                              | Success | 3               |
  | poly_tobytes                          | Success | 5               |
  | poly_tomont                           | Success | 7               |
  | poly_tomsg                            | Success | 6               |
  | polyvec_add                           | Success | 126             |
  | polyvec_basemul_acc_montgomery_cached | Success | 10              |
  | polyvec_frombytes                     | Success | 4               |
  | polyvec_mulcache_compute              | Success | 3               |
  | polyvec_reduce                        | Success | 4               |
  | polyvec_tobytes                       | Success | 3               |
  | rej_uniform                           | Success | 5               |
  | scalar_compress_q_16                  | Success | 3               |
  | scalar_compress_q_32                  | Success | 4               |
  | scalar_decompress_q_16                | Success | 3               |
  | scalar_decompress_q_32                | Success | 2               |
  | scalar_signed_to_unsigned_q_16        | Success | 3               |
  | unpack_pk                             | Success | 4               |

[hanno-becker]

Big hitters for K=4:

  | Proof                                 | Status  | Duration (in s) |
  |---------------------------------------|---------|-----------------|
  | barrett_reduce                        | Success | 4               |
  | basemul_cached                        | Success | 65              |
  | cmov_int16                            | Success | 4               |
  | fqmul                                 | Success | 13              |
  | gen_matrix_entry                      | Success | 126             |
  | montgomery_reduce                     | Success | 3               |
  | pack_pk                               | Success | 3               |
  | poly_add                              | Success | 4               |
  | poly_basemul_montgomery_cached        | Success | 254             |
  | poly_cbd_eta1                         | Success | 5               |
  | poly_cbd_eta2                         | Success | 4               |
  | poly_compress                         | Success | 4               |
  | poly_decompress                       | Success | 13              |
  | poly_frombytes                        | Success | 3               |
  | poly_getnoise_eta1122_4x              | Success | 6               |
  | poly_getnoise_eta1_4x                 | Success | 5               |
  | poly_getnoise_eta2                    | Success | 3               |
  | poly_getnoise_eta2_4x                 | Success | 2               |
  | poly_mulcache_compute                 | Success | 5               |
  | poly_reduce                           | Success | 4               |
  | poly_sub                              | Success | 7               |
  | poly_tobytes                          | Success | 6               |
  | poly_tomont                           | Success | 4               |
  | poly_tomsg                            | Success | 6               |
  | polyvec_add                           | Success | 1057            |
  | polyvec_basemul_acc_montgomery_cached | Success | 11              |
  | polyvec_frombytes                     | Success | 4               |
  | polyvec_mulcache_compute              | Success | 5               |
  | polyvec_reduce                        | Success | 5               |
  | polyvec_tobytes                       | Success | 5               |
  | rej_uniform                           | Success | 5               |
  | scalar_compress_q_16                  | Success | 4               |
  | scalar_compress_q_32                  | Success | 3               |
  | scalar_decompress_q_16                | Success | 4               |
  | scalar_decompress_q_32                | Success | 3               |
  | scalar_signed_to_unsigned_q_16        | Success | 3               |
  | unpack_pk                             | Success | 2               |

[hanno-becker]

It looks like we should really look at polyvec_add, but the others are still relatively fast. @mkannwischer