search

hacl-star / hacl-star

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

Blake2, 4/5: Extend specification to support last_node #934

Closed R1kM closed 1 month ago

R1kM commented 2 months ago

In addition to parameters, the Blake2 specification also supports a flag indicating the last node of a layer in tree-hashing mode. Similarly to hashing the last block, this has an impact on the compression function (see https://www.blake2.net/blake2.pdf, page 4).

This PR adds this feature to the Blake2 specification, as well as spec tests generated using the Python3 hashlib as an oracle. This PR does not expose an API to use it in the executed code, it only propagates spec changes to the verified implementation, setting the last_node flags to false.

github-actions[bot] commented 2 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.