-
Notifications
You must be signed in to change notification settings - Fork 160
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.
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
A preliminary version of HACL* extracted to *safe* Rust #918
base: main
Are you sure you want to change the base?
Conversation
ugh... the directory is a mix of hand-written files and autogenerated files, do I really need to manually list all the files that are hand-written? |
…r into afromher_rs
…keyword" This reverts commit 5201bad.
FYI CI is now green, and includes extracting, building and testing the Rust code. |
HACL packages CI is now green, which should allow us to get a perf comparison between:
@franziskuskiefer sounded like he would give this a stab, since eventually we want all of this to go into libcrux. |
Sorry, I missed the notifications about the Nix questions!
I know it is a bit tiresome, but this is really useful to avoid rebuilding when only the generated files change! |
@msprotz it seems like the source filter can be written a little bit more compactly, see https://github.com/hacl-star/hacl-star/tree/pnmadelaine/afromher_rs |
Awesome, can you submit a PR? |
Nix: simplify source filter for Rust extraction
Proposed changes
Preliminary support for Rust extraction of HACL*. This is joint work with @R1kM.
Enough work has gone into this that I would like to see things being put under CI so as to make sure nothing regresses.
I have no intention of advertising this as things are pretty rough still.This is now alpha-quality, with performance and APIs being the next things on our radar to fix.
Types of changes
This leverages the work of the past several months on the Rust backend of KaRaMeL and enables it within HACL*. Notably, this creates:
What to look for in this review
Limitations
Many of these modules compile, but have run-time errors.Most modules compile, test and fuzz without issues, but our toolchain does not guarantee the absence of runtime errors. @R1kM has a plan to fix this once and for all,but for now, only the addition of tests and/or fuzzing will help us figure out which modules have issues.which is on the radar.MoreA few leftover modules need to be rewritten to observe a buffer ownership pattern that is compatible with Rust.HMAC,HKDF, NaCl,Ed25519all require modifications in the source.More modules need to be rewritten to obey aliasing restrictions and avoid in-place APIs (Ed25519).