[CI] update code

include/Hacl_Hash_Blake2b.h

@@ -53,6 +53,24 @@ typedef struct Hacl_Hash_Blake2b_blake2_params_s
 }
 Hacl_Hash_Blake2b_blake2_params;
 
+typedef struct Hacl_Hash_Blake2b_index_s
+{
+ uint8_t key_length;
+ uint8_t digest_length;
+ bool last_node;
+}
+Hacl_Hash_Blake2b_index;
+
+#define HACL_HASH_BLAKE2B_BLOCK_BYTES (128U)
+
+#define HACL_HASH_BLAKE2B_OUT_BYTES (64U)
+
+#define HACL_HASH_BLAKE2B_KEY_BYTES (64U)
+
+#define HACL_HASH_BLAKE2B_SALT_BYTES (16U)
+
+#define HACL_HASH_BLAKE2B_PERSONAL_BYTES (16U)
+
 typedef struct K____uint64_t___uint64_t__s
 {
  uint64_t *fst;
@@ -64,7 +82,8 @@ typedef struct Hacl_Hash_Blake2b_block_state_t_s
 {
  uint8_t fst;
  uint8_t snd;
- K____uint64_t___uint64_t_ thd;
+ bool thd;
+ K____uint64_t___uint64_t_ f3;
 }
 Hacl_Hash_Blake2b_block_state_t;
 
@@ -92,7 +111,11 @@ The caller must satisfy the following requirements.
 
 */
 Hacl_Hash_Blake2b_state_t
-*Hacl_Hash_Blake2b_malloc_with_params_and_key(Hacl_Hash_Blake2b_blake2_params *p, uint8_t *k);
+*Hacl_Hash_Blake2b_malloc_with_params_and_key(
+ Hacl_Hash_Blake2b_blake2_params *p,
+ bool last_node,
+ uint8_t *k
+);
 
 /**
  Specialized allocation function that picks default values for all
@@ -116,7 +139,7 @@ Hacl_Hash_Blake2b_state_t *Hacl_Hash_Blake2b_malloc(void);
 
 /**
  General-purpose re-initialization function with parameters and
-key. You cannot change digest_length or key_length, meaning those values in
+key. You cannot change digest_length, key_length, or last_node, 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.
@@ -159,10 +182,14 @@ 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.
+length is whatever you chose for the `digest_length` field of your parameters.
+For convenience, this function returns `digest_length`. When in doubt, callers
+can pass an array of size HACL_BLAKE2B_32_OUT_BYTES, then use the return value
+to see how many bytes were actually written. 
 */
-void Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *state, uint8_t *output);
+uint8_t Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *s, uint8_t *dst);
+
+Hacl_Hash_Blake2b_index Hacl_Hash_Blake2b_info(Hacl_Hash_Blake2b_state_t *s);
 
 /**
  Free state function when there is no key
@@ -201,7 +228,7 @@ parameters `params` into `output`. The `key` array must be of length
 `params.digest_length`. 
 */
 void
-Hacl_Hash_Blake2b_hash_with_key_and_paramas(
+Hacl_Hash_Blake2b_hash_with_key_and_params(
  uint8_t *output,
  uint8_t *input,
  uint32_t input_len,

include/Hacl_Hash_Blake2b_Simd256.h

@@ -40,6 +40,16 @@ extern "C" {
 #include "Hacl_Hash_Blake2b.h"
 #include "libintvector.h"
 
+#define HACL_HASH_BLAKE2B_SIMD256_BLOCK_BYTES (128U)
+
+#define HACL_HASH_BLAKE2B_SIMD256_OUT_BYTES (64U)
+
+#define HACL_HASH_BLAKE2B_SIMD256_KEY_BYTES (64U)
+
+#define HACL_HASH_BLAKE2B_SIMD256_SALT_BYTES (16U)
+
+#define HACL_HASH_BLAKE2B_SIMD256_PERSONAL_BYTES (16U)
+
 typedef struct K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256__s
 {
  Lib_IntVector_Intrinsics_vec256 *fst;
@@ -51,7 +61,8 @@ 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;
+ bool thd;
+ K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ f3;
 }
 Hacl_Hash_Blake2b_Simd256_block_state_t;
 
@@ -64,34 +75,54 @@ 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).)
+ 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 256 for S, 64 for B.
+- The digest_length must not exceed 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,
+ bool last_node,
  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).
+ 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 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
+ 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_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.
+ General-purpose re-initialization function with parameters and
+key. You cannot change digest_length, key_length, or last_node, 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_Simd256_reset_with_key_and_params(
@@ -101,21 +132,27 @@ Hacl_Hash_Blake2b_Simd256_reset_with_key_and_params(
 );
 
 /**
- 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`
+ 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_Simd256_reset_with_key(Hacl_Hash_Blake2b_Simd256_state_t *s, uint8_t *k);
 
 /**
- Re-initialization function when there is no key
+ 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_Simd256_reset(Hacl_Hash_Blake2b_Simd256_state_t *s);
 
 /**
- Update function when there is no key; 0 = success, 1 = max length exceeded
+ Update function; 0 = success, 1 = max length exceeded
 */
 Hacl_Streaming_Types_error_code
 Hacl_Hash_Blake2b_Simd256_update(
@@ -125,18 +162,27 @@ Hacl_Hash_Blake2b_Simd256_update(
 );
 
 /**
- 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 256 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.
+For convenience, this function returns `digest_length`. When in doubt, callers
+can pass an array of size HACL_BLAKE2B_256_OUT_BYTES, then use the return value
+to see how many bytes were actually written. 
 */
-void
-Hacl_Hash_Blake2b_Simd256_digest(Hacl_Hash_Blake2b_Simd256_state_t *state, uint8_t *output);
+uint8_t Hacl_Hash_Blake2b_Simd256_digest(Hacl_Hash_Blake2b_Simd256_state_t *s, uint8_t *dst);
+
+Hacl_Hash_Blake2b_index Hacl_Hash_Blake2b_Simd256_info(Hacl_Hash_Blake2b_Simd256_state_t *s);
 
 /**
  Free state function when there is no key
 */
 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.
+ Copying. This preserves all parameters.
 */
 Hacl_Hash_Blake2b_Simd256_state_t
 *Hacl_Hash_Blake2b_Simd256_copy(Hacl_Hash_Blake2b_Simd256_state_t *state);
@@ -161,8 +207,14 @@ Hacl_Hash_Blake2b_Simd256_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_Simd256_hash_with_key_and_paramas(
+Hacl_Hash_Blake2b_Simd256_hash_with_key_and_params(
  uint8_t *output,
  uint8_t *input,
  uint32_t input_len,