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

C extraction for ML-DSA #710

Merged
merged 29 commits into from
Dec 16, 2024
Merged

C extraction for ML-DSA #710

merged 29 commits into from
Dec 16, 2024

Conversation

franziskuskiefer
Copy link
Member

@franziskuskiefer franziskuskiefer commented Dec 9, 2024 •
edited
Loading

This PR makes all necessary to extract C code from ML-DSA.

  • It updates the F* code that still laxes.
  • It includes a minimal self test.

To generate the C code, run

./c.sh --config cg.yaml --out cg --no-glue --no-unrolling --no-karamel_include --no-karamel_include --mldsa65

Follow ups

  • The generated code right now needs to be edited to remove the empty structs (see Drop (empty) unused structs AeneasVerif/eurydice#107).
  • The C boilerplate, tests, benchmarks need to be cleaned up in a follow up.
  • The avx2 variant may still have issues.
  • The stack size used by the C code is too large.

Note that this PR is on top of #707.
This works towards #706 but doesn't close it yet (see follow ups).

@franziskuskiefer
wip; started cleanup hashing
5642422
@franziskuskiefer
added shake256 xof
bf2b900 
and use it everywhere
@franziskuskiefer
F* extraction
7bf825a
@franziskuskiefer
wip
38bf469 
core.option.Option_c4 (found in file libcrux_core) mentions libcrux_ml_dsa.polynomial.PolynomialRingElement_24 (found in file libcrux_mldsa65_avx2)
@franziskuskiefer
more wip eurydice changes
5a0f22f
@franziskuskiefer
update for C extraction
76e8015
@franziskuskiefer
first C extraction
11a2dcf
@franziskuskiefer
more fixes for C (extracting but broken)
0273d4a
@franziskuskiefer
wip cg boilerplate
234b7d2
@franziskuskiefer
update serialize
8723dfe
@franziskuskiefer
more loop cleanups
b7df319
@franziskuskiefer
more loop cleanups
ce52b83
@franziskuskiefer
more loop cleanups
05d9103
@franziskuskiefer
more loop cleanups
3485de7
@franziskuskiefer
more cleanup for hax/eurydice
5686e51
@franziskuskiefer
extracting portable without eurydice failures
d0dff30
@franziskuskiefer
fixes for hax
d4b51bc
@franziskuskiefer
C and F* extraction
523b631
@franziskuskiefer
C extraction; not working
776fe1b
@franziskuskiefer
fix eurydice iterators
8749729
@franziskuskiefer
mldsa: feature guard sampling
02f1009
@franziskuskiefer
mldsa C code (portable working)
a93d7ea
@franziskuskiefer
mldsa: updated F* code
60ac469
@franziskuskiefer franziskuskiefer requested a review from a team as a code owner December 9, 2024 10:27
@franziskuskiefer franziskuskiefer self-assigned this Dec 9, 2024
keks
keks previously requested changes Dec 10, 2024
View reviewed changes
Copy link
Member

@keks keks left a comment

Choose a reason for hiding this comment

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

Some of my comments are nits, some a questions, but I think by and large this isn't controversial :)

libcrux-sha3/src/lib.rs Outdated Show resolved Hide resolved
libcrux-sha3/src/lib.rs Show resolved Hide resolved
libcrux-ml-dsa/src/hash_functions.rs Outdated Show resolved Hide resolved
libcrux-ml-dsa/src/hash_functions.rs Show resolved Hide resolved
libcrux-ml-dsa/src/ml_dsa_generic/instantiations/avx2.rs Outdated Show resolved Hide resolved
libcrux-ml-dsa/src/encoding/t1.rs Outdated Show resolved Hide resolved
libcrux-ml-dsa/src/matrix.rs Show resolved Hide resolved
Base automatically changed from franziskus/mldsa-c1 to main December 10, 2024 16:34
@github-actions github-actions bot dismissed keks’s stale review December 11, 2024 10:09

Review re-requested

keks
keks approved these changes Dec 16, 2024
View reviewed changes
Copy link
Member

@keks keks left a comment

Choose a reason for hiding this comment

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

I think this looks good and is ready to merge now, thanks! 👍

@franziskuskiefer franziskuskiefer added this pull request to the merge queue Dec 16, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Dec 16, 2024
@franziskuskiefer franziskuskiefer mentioned this pull request Dec 16, 2024
Merged
@franziskuskiefer franziskuskiefer added this pull request to the merge queue Dec 16, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to no response for status checks Dec 16, 2024
@franziskuskiefer franziskuskiefer added this pull request to the merge queue Dec 16, 2024
Merged via the queue into main with commit 5d76f68 Dec 16, 2024
52 checks passed
@franziskuskiefer franziskuskiefer deleted the franziskus/mldsa-c2 branch December 16, 2024 18:48
@franziskuskiefer franziskuskiefer mentioned this pull request Dec 20, 2024
Open
9 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@keks keks keks approved these changes

Assignees

@franziskuskiefer franziskuskiefer

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@franziskuskiefer @keks