Implement step 1 in #736:
Introduce a struct wrapper for the matrix: Instead of mld_polyvecl mat[MLDSA_K], use mld_polymat. This should follow pq-code-package/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.