CBMC: Add contracts and proofs for various polyvec functions

[mkannwischer]

• Depends on CBMC: Add contracts and proofs for various poly functions #140
• Resolves CBMC: Prove polyvecl_reduce #116
• Resolves CBMC: Prove polyvecl_add #117
• Resolves CBMC: Prove polyveck_reduce #124
• Resolves CBMC: Prove polyveck_add #126
• Resolves CBMC: Prove polyveck_sub #127
• Resolves CBMC: Prove polyveck_pack_w1 #136
• Resolves CBMC: Prove polyveck_use_hint #135

polyvecl_add, polyveck_add, polyveck_sub,polyveck_use_hint, polyveck_reduce, polyvecl_reduce were too slow when using unrolling - I instead did a direct proof with the workaround from #92. I added them to #102 to remove the whole-struct assignments once the corresponding CBMC issue is resolved.

[mkannwischer]

I removed the proofs from here that don't have acceptable run time yet and moved them to #169.
This way we can merge this one first.

[github-actions]

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Benchmark suite	Current: 6050f70	Previous: db0c059	Ratio
ML-DSA-44 keypair	305686 cycles	302258 cycles	1.01
ML-DSA-44 sign	1054556 cycles	1038859 cycles	1.02
ML-DSA-44 verify	328806 cycles	325882 cycles	1.01
ML-DSA-65 keypair	560506 cycles	557736 cycles	1.00
ML-DSA-65 sign	1549828 cycles	1517159 cycles	1.02
ML-DSA-65 verify	537579 cycles	532945 cycles	1.01
ML-DSA-87 keypair	863362 cycles	862513 cycles	1.00
ML-DSA-87 sign	1986410 cycles	1962426 cycles	1.01
ML-DSA-87 verify	894623 cycles	890895 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Benchmark suite	Current: 6050f70	Previous: db0c059	Ratio
ML-DSA-44 keypair	305610 cycles	302563 cycles	1.01
ML-DSA-44 sign	949111 cycles	1038239 cycles	0.91
ML-DSA-44 verify	329175 cycles	325625 cycles	1.01
ML-DSA-65 keypair	560411 cycles	557708 cycles	1.00
ML-DSA-65 sign	1543294 cycles	1521737 cycles	1.01
ML-DSA-65 verify	536667 cycles	533310 cycles	1.01
ML-DSA-87 keypair	865489 cycles	861766 cycles	1.00
ML-DSA-87 sign	1994548 cycles	1959841 cycles	1.02
ML-DSA-87 verify	897060 cycles	889017 cycles	1.01

This comment was automatically generated by workflow using github-action-benchmark.

[mkannwischer]

There is a measurable overhead of the whole-struct assignment CBMC workaround of 1-2% I'd say. That shouldn't stop us from proceeding, I think.

[mkannwischer]

This is ready for review now. Much pain.

[hanno-becker]

This is not going to work, and similar for poly_add, since the function is being called with aliasing first and second argument -- like in mlkem-native.

[hanno-becker]

poly_add, polyvecl_add, and polyveck_add are always called with first and second argument matching, which violates the current preconditions assuming them to be disjoint. The signature should be changed to the destructive version, as in mlkem-native.