x86: Add missing instructions for ML-KEM compressions#349
x86: Add missing instructions for ML-KEM compressions#349jargh merged 7 commits intoawslabs:mainfrom
Conversation
mkannwischer
force-pushed
the
mlkem-compression-instructions
branch
from
12d4967 to
be978fc
Compare
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
mkannwischer
force-pushed
the
mlkem-compression-instructions
branch
from
be978fc to
b2c883e
Compare
jargh
left a comment
jargh
left a comment
There was a problem hiding this comment.
All this looks great and all my tests are fine. It would be nice if you could also add a few more simulator test cases to sanity-check (1) memory versions of the new instructions where applicable, and (2) oversized immediates to check masking or otherwise where applicable. This patch gives a few examples that could be added. I don't consider this critical since I've already done so locally and confirmed they all seem fine, so if you are in a rush I can just approve anyway :-)
Thanks for the review! I'd appreciate if we can get it merged first and I'll add the additional tests in a follow-up PR later today. This way we can move forward in mlkem-native already. |
jargh
left a comment
jargh
left a comment
There was a problem hiding this comment.
OK, will now approve and merge
The vpmulhrsw and compression instruction support has been merged upstream (awslabs/s2n-bignum#349). Switch back from the fork to upstream awslabs/s2n-bignum@628a9cc. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Add simulator test patterns for VPSRLDQ, VPEXTRW, VPADDQ, VPACKUSWB, VPBLENDVB, VPMADDUBSW, and VPMADDWD, covering both register and memory operand variants. Proposed by @jargh in awslabs#349 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Add simulator test patterns for VPSRLDQ, VPEXTRW, VPADDQ, VPACKUSWB, VPBLENDVB, VPMADDUBSW, and VPMADDWD, covering both register and memory operand variants. Proposed by @jargh in awslabs#349 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
2 participants
Issue #, if available:
Description of changes:
This PR adds 7 additional missing AVX2 instructions that we require for the ML-KEM compressions. With those @hanno-becker was able to prove correctness of the 4 compression functions for d=4,5,10,11 (see pq-code-package/mlkem-native#1545). The 5 missing instructions for the 4 decompression functions proven in pq-code-package/mlkem-native#1543 were already added as a part of #346.
I ran the sematests for all instructions for a while, that plus the completed proofs give us some confidence that the instruction models are actually correct, but please take a look.
This completes the proofs of the arithmetic x86 backend of ML-KEM. 🎉🥳
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.