CBMC: Prove mld_polymat_permute_bitrev_to_custom on top of native API

[willieyz]

• Resolve: CBMC: Add proofs atop of native functions #350

• Related: Refactor mld_polymat_permute_bitrev_to_custom #770

• This PR refactor the polynomial matrix permutation logic by extracting a reusable mld_polyvecl_permute_bitrev_to_custom function and adds comprehensive CBMC verification for both C and native implementations.

• This is a temporary workaround until diffblue/cbmc#8796 is resolved.

• This PR made follwoing changes:

  • Extract mld_polyvecl_permute_bitrev_to_custom from mld_polymat_permute_bitrev_to_custom, and use polyvecl_permute_bitrev_to_custom's function contract in polymat_permute_bitrev_to_custom
  • Add CBMC contracts to mld_poly_permute_bitrev_to_custom in API header
  • Add CBMC proof for mld_polyvecl_permute_bitrev_to_custom (C implementation)
  • Add CBMC proof for mld_polyvecl_permute_bitrev_to_custom_native (native backend)

• Testing

  • make clean & MLD_CONFIG_PARAMETER_SET=44/65/87 make result checking the contract itself.
  • tests cbmc -p "parrent_proof", this will check the parrent proof

[mkannwischer]

The mld_polymat_permute_bitrev_to_custom needs to call the mld_polyvecl_permute_bitrev_to_custom function by contract, otherwise you are introducing a proof gap that the mld_polymat_permute_bitrev_to_custom isn't actually proven to be safe on top of the native backend.
The same problem exists in mlkem-native and should have been reported there rather than copied to mldsa-native. I opened a PR to fix that: pq-code-package/mlkem-native#1445.

[mkannwischer]

The code changes look good to me now.

Please clean up the commit message:
(1) The add changes seems to be an artifact of a squashed commit. You may want to use fixup rather than squash in such cases.
(2) From your current commit message no one can understand what you are trying to do. What you are doing is proving mld_polymat_permute_bitrev_to_custom on top of the native API. It should become clear why the refactoring is needed (pointing to the CBMC issue). It's often more important to describe why you are doing something in addition to what you are doing.
(3) The commit message is full of grammatical mistakes making it hard to follow. Please be more careful and consider spell-checking your commit messages.

[willieyz]

The code changes look good to me now.

Please clean up the commit message: (1) The add changes seems to be an artifact of a squashed commit. You may want to use fixup rather than squash in such cases. (2) From your current commit message no one can understand what you are trying to do. What you are doing is proving mld_polymat_permute_bitrev_to_custom on top of the native API. It should become clear why the refactoring is needed (pointing to the CBMC issue). It's often more important to describe why you are doing something in addition to what you are doing. (3) The commit message is full of grammatical mistakes making it hard to follow. Please be more careful and consider spell-checking your commit messages.

Hello, Matthias,
The changes have been updated. I have carefully cleaned up the commit history and revised the commit message to more clearly explain the goal, motivation, and reference the relevant CBMC issue.

Really appreciate your guidance and patience in reviewing this. Thank you very much.

[mkannwischer]

Thanks @willieyz! LGTM.