Merge pull request #461 from cryspen/franziskus/update-hacl-star

update hacl star

.github/workflows/gh-pages.yml

@@ -30,7 +30,7 @@ jobs:
 
       - name: Setup | System
         run: |
-          brew install doxygen sphinx-doc gmp ninja node
+          brew install doxygen gmp ninja node
           pip install --upgrade pip
 
       - name: Setup | OCaml | 1/2

benchmarks/sha3.cc

@@ -27,7 +27,8 @@ static void
 Hacl_Sha3_224(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_224(digest224.data(), (uint8_t*)input.data(), input.size());
+    Hacl_Hash_SHA3_sha3_224(
+      digest224.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest224 != expected_digest_sha3_224) {
     state.SkipWithError("Incorrect digest.");
@@ -51,7 +52,8 @@ static void
 Hacl_Sha3_256(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_256(digest256.data(), (uint8_t*)input.data(), input.size());
+    Hacl_Hash_SHA3_sha3_256(
+      digest256.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest256 != expected_digest_sha3_256) {
     state.SkipWithError("Incorrect digest.");
@@ -102,7 +104,8 @@ static void
 Hacl_Sha3_384(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_384(digest384.data(), (uint8_t*)input.data(), input.size());
+    Hacl_Hash_SHA3_sha3_384(
+      digest384.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest384 != expected_digest_sha3_384) {
     state.SkipWithError("Incorrect digest.");
@@ -126,7 +129,8 @@ static void
 Hacl_Sha3_512(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_512(digest512.data(), (uint8_t*)input.data(), input.size());
+    Hacl_Hash_SHA3_sha3_512(
+      digest512.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest512 != expected_digest_sha3_512) {
     state.SkipWithError("Incorrect digest.");
@@ -242,8 +246,10 @@ static void
 Hacl_Sha3_shake128(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_shake128_hacl(
-      input.size(), (uint8_t*)input.data(), digest_shake.size(), digest_shake.data());
+    Hacl_Hash_SHA3_shake128(digest_shake.data(),
+                            digest_shake.size(),
+                            (uint8_t*)input.data(),
+                            input.size());
   }
 }
 
@@ -253,8 +259,10 @@ static void
 Hacl_Sha3_shake256(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_shake256_hacl(
-      input.size(), (uint8_t*)input.data(), digest_shake.size(), digest_shake.data());
+    Hacl_Hash_SHA3_shake256(digest_shake.data(),
+                            digest_shake.size(),
+                            (uint8_t*)input.data(),
+                            input.size());
   }
 }
 

config/config.json

@@ -168,6 +168,10 @@
             {
                 "file": "Hacl_Hash_SHA3.c",
                 "features": "std"
+            },
+            {
+                "file": "Hacl_Hash_SHA3_Simd256.c",
+                "features": "vec256"
             }
         ],
         "sha2": [

docs/reference/hacl/hash/sha3.md

@@ -114,12 +114,12 @@ SHAKE128 and SHAKE256 have a 128- or 256-bit security strength and can produce a
 
 `````{tabs}
 ````{tab} 128-bit security strength
-```{doxygenfunction} Hacl_Hash_SHA3_shake128_hacl
+```{doxygenfunction} Hacl_Hash_SHA3_shake128
 ```
 ````
 
 ````{tab} 256-bit security strength
-```{doxygenfunction} Hacl_Hash_SHA3_shake256_hacl
+```{doxygenfunction} Hacl_Hash_SHA3_shake256
 ```
 ````
 `````

docs/reference/requirements.txt

@@ -1,8 +1,10 @@
+sphinx >= 5.0.0
+
 myst-parser
 sphinx-multiversion
 
 pydata-sphinx-theme
 sphinx-book-theme
 
 sphinx-tabs
-breathe==4.33.1
+breathe

include/Hacl_Ed25519.h

@@ -47,16 +47,16 @@ extern "C" {
 /**
 Compute the public key from the private key.
 
-  The outparam `public_key`  points to 32 bytes of valid memory, i.e., uint8_t[32].
-  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+  @param[out] public_key Points to 32 bytes of valid memory, i.e., `uint8_t[32]`. Must not overlap the memory location of `private_key`.
+  @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 */
 void Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key);
 
 /**
 Compute the expanded keys for an Ed25519 signature.
 
-  The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
-  The argument `private_key`   points to 32 bytes of valid memory, i.e., uint8_t[32].
+  @param[out] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`. Must not overlap the memory location of `private_key`.
+  @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 
   If one needs to sign several messages under the same private key, it is more efficient
   to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -66,11 +66,10 @@ void Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key);
 /**
 Create an Ed25519 signature with the (precomputed) expanded keys.
 
-  The outparam `signature`     points to 64 bytes of valid memory, i.e., uint8_t[64].
-  The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
-  The argument `msg`    points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
-
-  The argument `expanded_keys` is obtained through `expand_keys`.
+  @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `expanded_keys` nor `msg`.
+  @param[in] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`, containing the expanded keys obtained by invoking `expand_keys`.
+  @param[in] msg_len Length of `msg`.
+  @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
   If one needs to sign several messages under the same private key, it is more efficient
   to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -86,9 +85,10 @@ Hacl_Ed25519_sign_expanded(
 /**
 Create an Ed25519 signature.
 
-  The outparam `signature`   points to 64 bytes of valid memory, i.e., uint8_t[64].
-  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
-  The argument `msg`  points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+  @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `private_key` nor `msg`.
+  @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
+  @param[in] msg_len Length of `msg`.
+  @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
   The function first calls `expand_keys` and then invokes `sign_expanded`.
 
@@ -101,11 +101,12 @@ Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, ui
 /**
 Verify an Ed25519 signature.
 
-  The function returns `true` if the signature is valid and `false` otherwise.
+  @param public_key Points to 32 bytes of valid memory containing the public key, i.e., `uint8_t[32]`.
+  @param msg_len Length of `msg`.
+  @param msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
+  @param signature Points to 64 bytes of valid memory containing the signature, i.e., `uint8_t[64]`.
 
-  The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
-  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
-  The argument `signature`  points to 64 bytes of valid memory, i.e., uint8_t[64].
+  @return Returns `true` if the signature is valid and `false` otherwise.
 */
 bool
 Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature);

include/Hacl_Hash_Blake2b.h

@@ -38,11 +38,34 @@ extern "C" {
 #include "Hacl_Streaming_Types.h"
 #include "Hacl_Krmllib.h"
 
-typedef struct Hacl_Hash_Blake2b_block_state_t_s
+typedef struct Hacl_Hash_Blake2b_blake2_params_s
+{
+  uint8_t digest_length;
+  uint8_t key_length;
+  uint8_t fanout;
+  uint8_t depth;
+  uint32_t leaf_length;
+  uint64_t node_offset;
+  uint8_t node_depth;
+  uint8_t inner_length;
+  uint8_t *salt;
+  uint8_t *personal;
+}
+Hacl_Hash_Blake2b_blake2_params;
+
+typedef struct K____uint64_t___uint64_t__s
 {
   uint64_t *fst;
   uint64_t *snd;
 }
+K____uint64_t___uint64_t_;
+
+typedef struct Hacl_Hash_Blake2b_block_state_t_s
+{
+  uint8_t fst;
+  uint8_t snd;
+  K____uint64_t___uint64_t_ thd;
+}
 Hacl_Hash_Blake2b_block_state_t;
 
 typedef struct Hacl_Hash_Blake2b_state_t_s
@@ -54,23 +77,90 @@ typedef struct Hacl_Hash_Blake2b_state_t_s
 Hacl_Hash_Blake2b_state_t;
 
 /**
-  State allocation function when there is no key
+ General-purpose allocation function that gives control over all
+Blake2 parameters, including the key. Further resettings of the state SHALL be
+done with `reset_with_params_and_key`, and SHALL feature the exact same values
+for the `key_length` and `digest_length` fields as passed here. In other words,
+once you commit to a digest and key length, the only way to change these
+parameters is to allocate a new object.
+
+The caller must satisfy the following requirements.
+- The length of the key k MUST match the value of the field key_length in the
+  parameters.
+- The key_length must not exceed 32 for S, 64 for B.
+- The digest_length must not exceed 32 for S, 64 for B.
+
+*/
+Hacl_Hash_Blake2b_state_t
+*Hacl_Hash_Blake2b_malloc_with_params_and_key(Hacl_Hash_Blake2b_blake2_params *p, uint8_t *k);
+
+/**
+ Specialized allocation function that picks default values for all
+parameters, except for the key_length. Further resettings of the state SHALL be
+done with `reset_with_key`, and SHALL feature the exact same key length `kk` as
+passed here. In other words, once you commit to a key length, the only way to
+change this parameter is to allocate a new object.
+
+The caller must satisfy the following requirements.
+- The key_length must not exceed 32 for S, 64 for B.
+
+*/
+Hacl_Hash_Blake2b_state_t *Hacl_Hash_Blake2b_malloc_with_key(uint8_t *k, uint8_t kk);
+
+/**
+ Specialized allocation function that picks default values for all
+parameters, and has no key. Effectively, this is what you want if you intend to
+use Blake2 as a hash function. Further resettings of the state SHALL be done with `reset`.
 */
 Hacl_Hash_Blake2b_state_t *Hacl_Hash_Blake2b_malloc(void);
 
 /**
-  Re-initialization function when there is no key
+ General-purpose re-initialization function with parameters and
+key. You cannot change digest_length or key_length, meaning those values in
+the parameters object must be the same as originally decided via one of the
+malloc functions. All other values of the parameter can be changed. The behavior
+is unspecified if you violate this precondition.
+*/
+void
+Hacl_Hash_Blake2b_reset_with_key_and_params(
+  Hacl_Hash_Blake2b_state_t *s,
+  Hacl_Hash_Blake2b_blake2_params *p,
+  uint8_t *k
+);
+
+/**
+ Specialized-purpose re-initialization function with no parameters,
+and a key. The key length must be the same as originally decided via your choice
+of malloc function. All other parameters are reset to their default values. The
+original call to malloc MUST have set digest_length to the default value. The
+behavior is unspecified if you violate this precondition.
 */
-void Hacl_Hash_Blake2b_reset(Hacl_Hash_Blake2b_state_t *state);
+void Hacl_Hash_Blake2b_reset_with_key(Hacl_Hash_Blake2b_state_t *s, uint8_t *k);
 
 /**
-  Update function when there is no key; 0 = success, 1 = max length exceeded
+ Specialized-purpose re-initialization function with no parameters
+and no key. This is what you want if you intend to use Blake2 as a hash
+function. The key length and digest length must have been set to their
+respective default values via your choice of malloc function (always true if you
+used `malloc`). All other parameters are reset to their default values. The
+behavior is unspecified if you violate this precondition.
+*/
+void Hacl_Hash_Blake2b_reset(Hacl_Hash_Blake2b_state_t *s);
+
+/**
+  Update function; 0 = success, 1 = max length exceeded
 */
 Hacl_Streaming_Types_error_code
 Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint32_t chunk_len);
 
 /**
-  Finish function when there is no key
+ Digest function. This function expects the `output` array to hold
+at least `digest_length` bytes, where `digest_length` was determined by your
+choice of `malloc` function. Concretely, if you used `malloc` or
+`malloc_with_key`, then the expected length is 32 for S, or 64 for B (default
+digest length). If you used `malloc_with_params_and_key`, then the expected
+length is whatever you chose for the `digest_length` field of your
+parameters.
 */
 void Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *state, uint8_t *output);
 
@@ -79,6 +169,11 @@ void Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *state, uint8_t *output)
 */
 void Hacl_Hash_Blake2b_free(Hacl_Hash_Blake2b_state_t *state);
 
+/**
+  Copying. This preserves all parameters.
+*/
+Hacl_Hash_Blake2b_state_t *Hacl_Hash_Blake2b_copy(Hacl_Hash_Blake2b_state_t *state);
+
 /**
 Write the BLAKE2b digest of message `input` using key `key` into `output`.
 
@@ -99,6 +194,21 @@ Hacl_Hash_Blake2b_hash_with_key(
   uint32_t key_len
 );
 
+/**
+Write the BLAKE2b digest of message `input` using key `key` and
+parameters `params` into `output`. The `key` array must be of length
+`params.key_length`. The `output` array must be of length
+`params.digest_length`. 
+*/
+void
+Hacl_Hash_Blake2b_hash_with_key_and_paramas(
+  uint8_t *output,
+  uint8_t *input,
+  uint32_t input_len,
+  Hacl_Hash_Blake2b_blake2_params params,
+  uint8_t *key
+);
+
 #if defined(__cplusplus)
 }
 #endif