[CI] update code

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

include/Hacl_Hash_Blake2b_Simd256.h

@@ -37,13 +37,22 @@ extern "C" {
 
 #include "Hacl_Streaming_Types.h"
 #include "Hacl_Krmllib.h"
+#include "Hacl_Hash_Blake2b.h"
 #include "libintvector.h"
 
-typedef struct Hacl_Hash_Blake2b_Simd256_block_state_t_s
+typedef struct K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256__s
 {
  Lib_IntVector_Intrinsics_vec256 *fst;
  Lib_IntVector_Intrinsics_vec256 *snd;
 }
+K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_;
+
+typedef struct Hacl_Hash_Blake2b_Simd256_block_state_t_s
+{
+ uint8_t fst;
+ uint8_t snd;
+ K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ thd;
+}
 Hacl_Hash_Blake2b_Simd256_block_state_t;
 
 typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s
@@ -54,15 +63,56 @@ typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s
 }
 Hacl_Hash_Blake2b_Simd256_state_t;
 
+/**
+ State allocation function when there are parameters and a key. The
+length of the key k MUST match the value of the field key_length in the
+parameters. Furthermore, there is a static (not dynamically checked) requirement
+that key_length does not exceed max_key (256 for S, 64 for B).)
+*/
+Hacl_Hash_Blake2b_Simd256_state_t
+*Hacl_Hash_Blake2b_Simd256_malloc_with_params_and_key(
+ Hacl_Hash_Blake2b_blake2_params *p,
+ uint8_t *k
+);
+
+/**
+ State allocation function when there is just a custom key. All
+other parameters are set to their respective default values, meaning the output
+length is the maximum allowed output (256 for S, 64 for B).
+*/
+Hacl_Hash_Blake2b_Simd256_state_t
+*Hacl_Hash_Blake2b_Simd256_malloc_with_key0(uint8_t *k, uint8_t kk);
+
 /**
  State allocation function when there is no key
 */
 Hacl_Hash_Blake2b_Simd256_state_t *Hacl_Hash_Blake2b_Simd256_malloc(void);
 
+/**
+ Re-initialization function. The reinitialization API is tricky --
+you MUST reuse the same original parameters for digest (output) length and key
+length.
+*/
+void
+Hacl_Hash_Blake2b_Simd256_reset_with_key_and_params(
+ Hacl_Hash_Blake2b_Simd256_state_t *s,
+ Hacl_Hash_Blake2b_blake2_params *p,
+ uint8_t *k
+);
+
+/**
+ Re-initialization function when there is a key. Note that the key
+size is not allowed to change, which is why this function does not take a key
+length -- the key has to be same key size that was originally passed to
+`malloc_with_key`
+*/
+void
+Hacl_Hash_Blake2b_Simd256_reset_with_key(Hacl_Hash_Blake2b_Simd256_state_t *s, uint8_t *k);
+
 /**
  Re-initialization function when there is no key
 */
-void Hacl_Hash_Blake2b_Simd256_reset(Hacl_Hash_Blake2b_Simd256_state_t *state);
+void Hacl_Hash_Blake2b_Simd256_reset(Hacl_Hash_Blake2b_Simd256_state_t *s);
 
 /**
  Update function when there is no key; 0 = success, 1 = max length exceeded
@@ -85,6 +135,12 @@ Hacl_Hash_Blake2b_Simd256_digest(Hacl_Hash_Blake2b_Simd256_state_t *state, uint8
 */
 void Hacl_Hash_Blake2b_Simd256_free(Hacl_Hash_Blake2b_Simd256_state_t *state);
 
+/**
+ Copying. The key length (or absence thereof) must match between source and destination.
+*/
+Hacl_Hash_Blake2b_Simd256_state_t
+*Hacl_Hash_Blake2b_Simd256_copy(Hacl_Hash_Blake2b_Simd256_state_t *state);
+
 /**
 Write the BLAKE2b digest of message `input` using key `key` into `output`.
 
@@ -105,6 +161,15 @@ Hacl_Hash_Blake2b_Simd256_hash_with_key(
  uint32_t key_len
 );
 
+void
+Hacl_Hash_Blake2b_Simd256_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