hacl-star / hacl-star

HACL*, a formally verified cryptographic library written in F*
Apache License 2.0
1.62k stars 168 forks source link

Remove unneeded branch in K256 #925

Closed R1kM closed 5 months ago

R1kM commented 6 months ago

Proposed changes

This PR removes dead code in K256: in the current code, a branch was checking if a UInt64 was strictly greater than U64_MAX. Note, I would expect the C compiler to detect this and optimize the branch away, so I don't expect any changes in performance (but didn't measure this). I found this issue while porting K256 to Rust, where the Rust compiler raised a warning for the resulting code.

github-actions[bot] commented 6 months ago

[CI] Important! The code in dist/gcc-compatible, dist/msvc-compatible, and dist/wasm is tested on cryspen/hacl-packages. dist is not automatically re-generated, be sure to do it manually. (A fresh snapshot can also be downloaded from CI by going to the "artifacts" section of your run.) Then check the following tests before merging this PR. Always check the latest run, it corresponds to the most recent version of this branch. All jobs are expected to be successful. In some cases manual intervention is needed. Please ping the hacl-packages maintainers.