Feedback on rust code

[ctz]

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:

#[inline] fn sha256_update(b: &mut [u8], hash: &mut [u32]) -> ()

The b parameter here need not be mutable. That has contagion all the way to the "top" of the API (for example) in evercrypt::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 than usize, for example in

#[inline] fn update_224_256(
    state: &mut [crate::hacl::streaming_types::state_32],
    chunk: &[u8],
    chunk_len: u32
) ->

That is mostly a stylistic issue though.

4/ Some mysterious subexpressions clippy found:

warning: this operation has no effect
    --> src/hacl/bignum.rs:1124:66
     |
1124 |         (&mut acc)[0usize] = beq & (&mut acc)[0usize] | ! beq & (blt & 0xFFFFFFFFu32 | ! blt & 0u32)
     |                                                                  ^^^^^^^^^^^^^^^^^^^ help: consider reducing it to: `blt`
     |

error: this operation will always return zero. This is likely not the intended outcome
    --> src/hacl/bignum.rs:1124:88
     |
1124 |         (&mut acc)[0usize] = beq & (&mut acc)[0usize] | ! beq & (blt & 0xFFFFFFFFu32 | ! blt & 0u32)
     |                                                                                        ^^^^^^^^^^^^
     |

5/ Post-generation, it would be good to run the code through rustfmt to normalise the formatting.

[R1kM]

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.