CBMC: Prove mld_polymat_permute_bitrev_to_custom on top of native API #820
+189
−16
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
willieyz
force-pushed
the
cbmc-bitrev-to-custom-workarounds
branch
2 times, most recently
from
3246468 to
ae1ed8d
Compare
willieyz
changed the title
mkannwischer
requested changes
Jan 1, 2026
Contributor
mkannwischer
left a comment
mkannwischer
left a comment
There was a problem hiding this comment.
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.
- This commit apply same workarounds for
mld_polymat_permute_bitrev_to_custom, reference from mlkem-native,
add following function and corresponding CBMC proof:
- mld_polyvecl_permute_bitrev_to_custom
- mld_polyvecl_permute_bitrev_to_custom_native
- and for the CBMC proof for above function:
- mld_polyvecl_permute_bitrev_to_custom_native
we add the contract and exception in check-contracts for
for mld_poly_permute_bitrev_to_custom.
- Use tests cbmc -p polymat_permute_bitrev_to_custom contract in
polymat_permute_bitrev_to_custom cbmc proof
Signed-off-by: willieyz <willie.zhao@chelpis.com>
add changes
Signed-off-by: willieyz <willie.zhao@chelpis.com>
willieyz
force-pushed
the
cbmc-bitrev-to-custom-workarounds
branch
from
ae1ed8d to
6fef01b
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Resolve: CBMC: Add proofs atop of native functions #350
Related: CBMC proofs for mld_poly_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:
Testing
make clean & MLD_CONFIG_PARAMETER_SET=44/65/87 make resultchecking the contract itself.tests cbmc -p "parrent_proof", this will check the parrent proof