[Test] Namespacing: Add MLD_CONFIG_PARAMETER_SET + MLD_CONFIG_NAMESPACE_PREFIX

[jakemas]

CI testing

[jakemas]

Do the -87 proofs need more memory? If so which? Why is CI hanging ... why won't it tell me where it hung?

I'll up polyvecl_pointwise_acc_montgomery to 9 CBMC bits...

Reproducing locally, It still seems to be stalling on polyvec_matrix_expand is it to do with the anti-pattern namspacing of mld_poly_permute_bitrev_to_custom used within the contract?

#if !defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER)
/* This namespacing is not done at the top to avoid a naming conflict
 * with native backends, which are currently not yet namespaced. */
#define mld_poly_permute_bitrev_to_custom \
  MLD_NAMESPACE(mld_poly_permute_bitrev_to_custom)

static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t data[MLDSA_N])
{
  ((void)data);
}
#endif /* !MLD_USE_NATIVE_NTT_CUSTOM_ORDER */

[jakemas]

polyvec_matrix_expand is a good proof to test locally, as reproducibility was good here. For me, CBMC bits < 12 would fail. Hypothesis, the use function contracts may not be inlining contracts correctly (because of the namespacing), and causing proofs to blow up. Not when I run make result in the directory, but when running test cbmc.