CBMC: Don't declare arrays in harnesses

When CBMC checks a function contract, it seems that the preconditions
set out in the contract are overlayed by the context set out in the
harness. For example, if a function takes a pointer to `foo`, and the
harness passes `&f` for `foo f`, then the function would never be
evaluated for the possibility of an invalid pointer being passed.
For that reason, harnesses must be as minimal as possible, merely
declaring uninitialized variables of the expected type and calling
the function under proof.

This commit fixes a few instances in mlkem-native where this was
not yet the case.

Signed-off-by: Hanno Becker <[email protected]>

Author: hanno-becker

proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c

@@ -9,6 +9,6 @@ void mlk_poly_permute_bitrev_to_custom(int16_t data[MLKEM_N]);
 
 void harness(void)
 {
-  int16_t data[MLKEM_N];
+  int16_t *data;
   mlk_poly_permute_bitrev_to_custom(data);
 }

proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c

@@ -7,7 +7,7 @@
 
 void harness(void)
 {
-  mlk_poly out[4];
-  uint8_t seed[4][MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];
+  mlk_poly *out;
+  uint8_t(*seed)[MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];
   mlk_poly_rej_uniform_x4(out, seed);
 }