CBMC: Refactor `mld_polymat_permute_bitrev_to_custom` and prove monolithically

[mkannwischer]

See pq-code-package/mlkem-native#1375.

#820 split up mld_polymat_permute_bitrev_to_custom into two separate functions so that CBMC proofs can be achieved on top of the native API. Once diffblue/cbmc#8796 is resolved, we should undo the refactoring and prove mld_polymat_permute_bitrev_to_custom in one piece.

[mkannwischer]

@willieyz, can you already rebase and update #770, please? We should get the CBMC proofs to work in the PR based on the experimental CBMC.

[willieyz]

@willieyz, can you already rebase and update #770, please? We should get the CBMC proofs to work in the PR based on the experimental CBMC.

Hello @mkannwischer,
I have rebased #770 on top of #820.
During the rebase, I removed mld_polyvecl_permute_bitrev_to_custom from mldsa-native since it was a workaround.
I would appreciate it if you could take a look and let me know whether this aligns with your expectations.