CBMC: Refactor `mlk_polymat_permute_bitrev_to_custom` and prove monolithically

https://github.com/pq-code-package/mldsa-native/pull/770 suggests that `mlk_polymat_permute_bitrev_to_custom` can be proven monolithically once https://github.com/diffblue/cbmc/issues/8796 is resolved.
We should also refactor it in mlkem-native.