CBMC: Some minor clean-up

[mkannwischer]

This is a series of small improvements to the CBMC annotations and proofs that I have been holding back.

I'd like your opinion particularly on the first commit: We can remove all loop annotations in the relatively simple loops in polyvec.c. I very much prefer fewer annotations in code.

The reason, this didn't actually work before was that we got the loop index wrong. Functions like POLYVEC_UBOUND are defined as an empty while loop in debug.h and, hence, count as a loop for CBMC.

There are potentially more places where this can help.

[mkannwischer]

I double checked that c10c3f7 had no impact on the proof run-time of

• polyvec_compress_du
• polyvec_decompress_du
• polyvec_tobytes

• polyvec_basemul_acc_montgomery_cached

  These all take a few seconds only.

[hanno-becker]

I agree that annotations should be kept to a minimum. If a loop can simply be fully unrolled without incurring a meaningful performance cost, we should do that.