CBMC: Cover `mld_polymat` with `MLD_CONFIG_REDUCE_RAM` set

[mkannwischer]

#742 introduced the option to sample the polynomial matrix on-the-fly. This requires changing the struct definition of mld_polymat.

I believe that means we have the following options to cover MLD_CONFIG_REDUCE_RAM:
(1) We run all CBMC proofs w/ and w/o MLD_CONFIG_REDUCE_RAM set. That seems the safest, but most expensive option.

(2) We only re-run the CBMC proofs that make use of mld_polymat. Those are:

• mld_polyvec_matrix_pointwise_montgomery (which inlines mld_polymat_get_row)
• mld_compute_t0_t1_tr_from_sk_components
• mld_attempt_signature_generation
• crypto_sign_signature_internal
• crypto_sign_verify_internal

For option (2), I see two implementation choices:
(2a) Duplicate the relevant proofs and add a _reduced_ram post-fix - similar as we currently do for the native functions.
(2b) Do not duplicate the proofs, but instead place a marker file into the proof directory triggering it to be run with multiple configurations. If we head down this route, it would be good if we could cover the other cases (native, serial, big-endian) at the same time.

Any thoughts on the best way to take here @hanno-becker?