Switch mlk_polyvec and mlk_polymat to struct wrappers #1115
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
Contributor
hanno-becker
commented
Jul 9, 2025
hanno-becker
commented
- Change mlk_polyvec back to struct { mlk_poly vec[MLKEM_K]; }
- Change mlk_polymat to struct { mlk_polyvec vec[MLKEM_K]; }
- Update all function signatures to use pointer style
- Fix all implementations to use struct member access
- Update tests, benchmarks, and CBMC harnesses
- Add consistent const annotations
|
@rod-chapman suggested that this unblocks #906. Adjusting it to check if that's true. |
Should this be converted to a draft PR in that case? |
|
@mkannwischer We could. One could make the argument, though, that the only reason to introduce |
- Change mlk_polyvec back to struct { mlk_poly vec[MLKEM_K]; }
- Change mlk_polymat to struct { mlk_polyvec vec[MLKEM_K]; }
- Update all function signatures to use pointer style
- Fix all implementations to use struct member access
- Update tests, benchmarks, and CBMC harnesses
- Add consistent const annotations
Signed-off-by: Hanno Becker <[email protected]>
Previously, the base multiplication would assume that one of its inputs
is bound by 4096 in absolute value, but make no assumptions about the
other input ("b-input" henceforth) and its mulcache.
This commit refines the bounds slightly, as follows:
- The b-input is assumed to be bound by MLK_NTT_BOUND in absolute value.
This comes for free since all values for b _are_ results of the NTT.
- The b-cache-input is assumed to be bound by MLKEM_Q in absolute value.
With those additional bounds in place, it can be showed that the result
of the base multiplication is below INT16_MAX/2 in absolute value.
Accordingly, this can be added as a precondition for the inverse NTT.
Those refined bounds can help in subsequent commits to improve the
reduction strategy inside the inverse NTT.
For the native AVX2 backend, the new output bound for the mulcache
forces an explicit zeroization of the mulcache. This is not ideal
since the cache is in fact entirely unused, but the performance
penalty should be marginal (if the compiler can't eliminate the
zeroization in the first place).
Signed-off-by: Hanno Becker <[email protected]>
Signed-off-by: Rod Chapman <[email protected]>
|
Does this change improve performance and/or stability of proof on platforms that we care about (by which I really mean - AArch64/macOS, Intel/Linux, EC2 Graviton/Linux, and "whatever our CI runners are running..."? I assume performance impact on generated code is negligible? |
|
Closing this for now. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.