CBMC: Refactor `mlk_polymat_permute_bitrev_to_custom` and prove monolithically

[mkannwischer]

pq-code-package/mldsa-native#770 suggests that mlk_polymat_permute_bitrev_to_custom can be proven monolithically once diffblue/cbmc#8796 is resolved.
We should also refactor it in mlkem-native.