Reduce RAM usage by streaming matrix

[hanno-becker]

Goal: The goal of this task is to reduce RAM usage by ad-hoc generating the matrix rather than storing it in memory.

Proposed steps (these should be critiqued):

• Introduce a struct wrapper for the matrix: Instead of mld_polyvecl mat[MLDSA_K], use mld_polymat. This should follow Reintroduce struct definitions for mlk_poly{mat,vec} mlkem-native#1263. Check that tests all still pass. Adjust all CBMC annotations and check the relevant proofs via tests cbmc -p {FUNCTION_NAME}, to be run in the nix develop shell. See tests cbmc --list-functions for the full list of functions.
• Introduce a helper function mld_polymat_get_row which retrieves a mld_polyvecl pointer from a mld_polymat pointer pointing to the required row of the matrix. Initially, this would simply return the address of the i-th entry in the mld_polyvecl mat[MLDSA_K] array that mld_polymat wraps. Rewrite mld_polyvec_matrix_pointwise_montgomery() to use this function rather than directly accessing the matrix. Check that ./scripts/tests all still passes. Adjust all CBMC annotations and check the relevant proofs via tests cbmc -p {FUNCTION_NAME}, to be run in the nix develop shell. See tests cbmc --list-functions for the full list of functions.
• Check that at this point, the only operations dealing with the matrix are (a) mld_polymat_get_row(), (b) mld_polyvec_matrix_expand(), (c) mld_polyvec_matrix_pointwise_montgomery(), and (d) mld_polymat_permute_bitrev_to_custom().
• Introduce a compile-time option MLD_CONFIG_REDUCE_RAM. It should be unset by default. Initially, it should be unused.
• Implement MLD_CONFIG_REDUCE_RAM, ignoring CBMC initially:
  • Modify the definition of mld_polymat so it contains a single mld_polyvecl and a copy of the seed-buffer const uint8_t rho[MLDSA_SEEDBYTES].
  • mld_polyvec_matrix_expand() should merely copy the seed buffer. Note that this changes the signature of mld_polyvec_matrix_pointwise_montgomery as it can no longer take the matrix as const.
  • mld_polymat_get_row() should ad-hoc generate the required row by calling mld_poly_uniform in a loop, just as in mld_polyvec_matrix_expand(), and call mld_poly_permute_bitrev_to_custom on the generated entries to make sure they have the right ordering. Initially, this should ignore batched matrix generation, at the cost of performance.
  • mld_polyvec_matrix_pointwise_montgomery() does not need changing since it already calls mld_polymat_get_row().
  • Make sure ./scripts/tests all still passes, but ignore CBMC annotations and proofs in this step.
• Verify the reduction in stack usage when MLD_CONFIG_REDUCE_RAM is used and document it.
• TBD: Develop and implement a test plan for MLD_CONFIG_REDUCE_RAM.
• TBD: Find a way to make CBMC happy