Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Making ML-KEM Extract Again #308

Merged
merged 14 commits into from
Jun 12, 2024
Merged

Making ML-KEM Extract Again #308

merged 14 commits into from
Jun 12, 2024

Conversation

karthikbhargavan
Copy link
Contributor

This PR does some changes to make the new ML-KEM code extract to F*.
This does not lax typecheck yet.

franziskuskiefer
franziskuskiefer requested changes Jun 11, 2024
View reviewed changes
Copy link
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This needs some formatting.

Looks like hax is failing. Can we get that fixed so that it's actually extracting?

libcrux-ml-kem/src/constants.rs Outdated Show resolved Hide resolved
@msprotz msprotz mentioned this pull request Jun 11, 2024
Merged
@franziskuskiefer franziskuskiefer linked an issue Jun 12, 2024 that may be closed by this pull request
ML-KEM SIMD F* Extraction #269
Closed
@franziskuskiefer
Copy link
Member

I checked performance and couldn't measure a difference in Rust or C.
I updated the C extraction with AeneasVerif/eurydice#25 and added a small helper for build after getting tired of calling cmake directly all the time.

The hax CI needs to get fixed and we need to re-enable the extraction of this crate on CI.

@franziskuskiefer franziskuskiefer mentioned this pull request Jun 12, 2024
Closed
@franziskuskiefer franziskuskiefer merged commit 664dc26 into dev Jun 12, 2024
41 checks passed
@franziskuskiefer franziskuskiefer deleted the franziskus/hax-extract-ml-kem branch June 12, 2024 07:12
@karthikbhargavan karthikbhargavan mentioned this pull request Jun 12, 2024
Merged
@franziskuskiefer franziskuskiefer mentioned this pull request Jun 12, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@franziskuskiefer franziskuskiefer franziskuskiefer approved these changes

Assignees
No one assigned
Labels
None yet
Projects
libcrux
Status: ✅ Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

ML-KEM SIMD F* Extraction
2 participants
@karthikbhargavan @franziskuskiefer