-
Notifications
You must be signed in to change notification settings - Fork 161
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
Feedback on rust code #944
Comments
Thank you very much for your interest and your feedback! Regarding your different points: 1/ Indeed, we are for now overly conservative about generating mutable instead of shared borrows for slices. We are currently working on a static analysis pass during extraction to (hopefully) heavily reduce the number of unneeded mutable borrows. 2/ This is a slightly more involved change as our verified code currently requires extracting to both C and Rust, and this length information is unavailable in C. We are not sure yet whether there would be a technical solution improving the generated Rust code while preserving without impacting the C extraction. 3/ This is unfortunately due to the memory model used for verification, and would also be a fairly involved change impacting the entire codebase (and other verification projects using F*). 4/ This is surprising, we will investigate. Additionally, we plan to improve code generation to be compliant with clippy, but did not get to it yet. 5/ That's a good point, we'll look into adding it to both our CI and codegen Makefiles. |
Hello!
I've been looking over https://github.com/hacl-star/hacl-star/tree/afromher_rs/dist/rs/src linked from https://jonathan.protzenko.fr/2024/03/20/hacl-rs.html.
Very interested in having a verified, pure rust cryptography library, so this is exciting.
Some comments:
1/ There seems to be an unnecessary use of mutable slices for inputs. For example:
The
b
parameter here need not be mutable. That has contagion all the way to the "top" of the API (for example) inevercrypt::hash::update
. It would mean that all inputs (which would invariably be non-mutable slices) would need to be copied before being used in this API.2/ Slices know about their own length. So there is not a need to duplicate this length into a separate parameter (for example:
hmac::compute_sha2_256
second+third & fourth+fifth parameters).3/
u32
is used as a length quantity rather thanusize
, for example inThat is mostly a stylistic issue though.
4/ Some mysterious subexpressions clippy found:
5/ Post-generation, it would be good to run the code through
rustfmt
to normalise the formatting.The text was updated successfully, but these errors were encountered: