Refactor mlk_polymat_permute_bitrev_to_custom

[mkannwischer]

• Resolves CBMC: Refactor mlk_polymat_permute_bitrev_to_custom and prove monolithically #1375

This commit refactors mlk_polymat_permute_bitrev_to_custom to not require the helper function mlk_polyvec_permute_bitrev_to_custom. The function was only needed due CBMC limitations.

[mkannwischer]

This proves fine in a couple of seconds for MLKEM_K=3, but spins forever for MLKEM_K=2 and MLKEM_K=4:

$ tests cbmc -p polymat_permute_bitrev_to_custom_native --k 3

For your convenience, the output of this run will be symbolically linked to  /Users/matthiaskannwischer/git/native/mlkem-native/proofs/cbmc/output/latest/html/index.html 

Configuring CBMC proofs: 1 / 1
[16/16] mlk_polymat_permute_bitrev_to_custom_native: generating report                                                                                                                                                                                                                                                                                                  
Report was rendered at file:///Users/matthiaskannwischer/git/native/mlkem-native/proofs/cbmc/output/latest/html/index.html
## Summary of CBMC proof results

| Status  | Count |
|---------|-------|
| Success | 1     |

| Proof                                       | Status  | Duration (in s) |
|---------------------------------------------|---------|-----------------|
| mlk_polymat_permute_bitrev_to_custom_native | Success | 6               |


WARNING:root:$GITHUB_STEP_SUMMARY not set, not writing summary file
All good!
Matthiass-MacBook-Pro:mlkem-native matthiaskannwischer$ tests cbmc -p polymat_permute_bitrev_to_custom_native --k 2

For your convenience, the output of this run will be symbolically linked to  /Users/matthiaskannwischer/git/native/mlkem-native/proofs/cbmc/output/latest/html/index.html 

Configuring CBMC proofs: 1 / 1
[14/16] mlk_polymat_permute_bitrev_to_custom_native: printing safety properties  

Makes no sense to me.
@rod-chapman, any ideas?

[rod-chapman]

Since we introduced struct wrappers around mlk_polyvec and mlk_polymat, the latter is now a struct that contains a K-element array of structs, each of which contains a single K-element array of mlk_poly.

This new code is trying to treat that as a single-dimensional array of K*K mlk_poly's by the look of it. That's bound to cause serious complications for CBMC.

Try a nested loop, so the code structure matches the data structure.

[hanno-becker]

@mkannwischer Can you comment on state/plans for this?

[mkannwischer]

@mkannwischer Can you comment on state/plans for this?

See pq-code-package/mldsa-native#770 - we are waiting for diffblue/cbmc#8705 to be merged.

@willieyz, could you rebase this PR and also include the experimental branch of CBMC so we can confirm that the proofs pass with that version.

[willieyz]

@mkannwischer Can you comment on state/plans for this?

See pq-code-package/mldsa-native#770 - we are waiting for diffblue/cbmc#8705 to be merged.

@willieyz, could you rebase this PR and also include the experimental branch of CBMC so we can confirm that the proofs pass with that version.

Yes, I can do it.

[hanno-becker]

This seems no longer relevant; closing. @mkannwischer reopen if you disagree and foresee time to work on this.

[mkannwischer]

This seems no longer relevant; closing. @mkannwischer reopen if you disagree and foresee time to work on this.

Why is this no longer relevant? I still want to do this refactoring as soon as the CBMC fix has been merged.

[rod-chapman]

Agree. We will return to this when we get a new release of CBMC. The helper function could be removed if and when CBMC can handle a nested loop efficiently.