A preliminary version of HACL* extracted to *safe* Rust

[msprotz]

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:

• a new subdirectory, dist/rs
• puts under version control a complete extraction of HACL* to Rust, modulo KaRaMeL failures for some of the functions
• adds some hand-written files for the library modules (hacl.rs, lib.rs, etc.), the machine integers (eventually should be extracted, but hand-written for now)
• adds targets in the main Makefile to extract and build with cargo

What to look for in this review

• Many small, non-threatening changes had to be enacted on the original F* source in order to comply with the restrictions of the Rust borrow-checker. As such, the first thing to review is the diff for dist/gcc-compatible; I would need some performance benchmarks to make sure there are no regressions.
• Then, one can look at the shape of the generated Rust code, the build, and debate whether this is an acceptable layout, etc.

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.
• More A few leftover modules need to be rewritten to observe a buffer ownership pattern that is compatible with Rust. HMAC, HKDF, NaCl, Ed25519 all require modifications in the source.
• More modules need to be rewritten to obey aliasing restrictions and avoid in-place APIs (Ed25519).
• There are likely many performance issues, the chief one that I'm aware of being the fact that we take mutable pointers to globally-allocated constants, which generates a copy of the constant per the corresponding Rust warning. This is quite concerning, and I don't know if this will be optimized at the LLVM level. In any case, this is something I'd like to fix. While we could try to port the source to leverage LowStar.ConstBuffer more, this is likely going to be a herculean task, and I'd rather implement a const-analysis phase in krml in order to automatically decorate all pointers (and function signatures) with const whenever possible. It's still a fair amount of work, but not as bad as fixing the source.

[msprotz]

the source files that make it into the Nix build are filtered here:

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?

[msprotz]

FYI CI is now green, and includes extracting, building and testing the Rust code.

[msprotz]

HACL packages CI is now green, which should allow us to get a perf comparison between:

• HACL/main and HACL/afromher_rs, in C -- how much do the source changes on this branch slow down the C code? see "Run benchmarks" in the hacl-packages CI (link in the first comment), or see https://github.com/cryspen/hacl-packages/actions/runs/8403105166/job/23013244329 for a sample run; slowdowns for bignum operations and blake2
• HACL/afromher_rs, in C vs. HACL/afromher_rs, in Rust -- how much slower are the Rust versions?

@franziskuskiefer sounded like he would give this a stab, since eventually we want all of this to go into libcrux.

[pnmadelaine]

Sorry, I missed the notifications about the Nix questions!

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?

I know it is a bit tiresome, but this is really useful to avoid rebuilding when only the generated files change!

[pnmadelaine]

@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

[msprotz]

Awesome, can you submit a PR?