From 36510e386be2df659bcb2739b47890e7dc014340 Mon Sep 17 00:00:00 2001 From: Hacl Bot Date: Sun, 7 Apr 2024 00:42:25 +0000 Subject: [PATCH] [CI] update code --- include/Hacl_Ed25519.h | 33 ++++---- include/internal/Hacl_Hash_Blake2b.h | 15 ++++ include/internal/Hacl_Hash_Blake2b_Simd256.h | 1 + include/internal/Hacl_Hash_Blake2s.h | 1 + include/internal/Hacl_Hash_Blake2s_Simd128.h | 1 + include/lib_memzero0.h | 2 +- include/msvc/Hacl_Ed25519.h | 33 ++++---- include/msvc/internal/Hacl_Hash_Blake2b.h | 15 ++++ .../msvc/internal/Hacl_Hash_Blake2b_Simd256.h | 1 + include/msvc/internal/Hacl_Hash_Blake2s.h | 1 + .../msvc/internal/Hacl_Hash_Blake2s_Simd128.h | 1 + include/msvc/lib_memzero0.h | 2 +- ocaml/lib/Hacl_Hash_Blake2b_bindings.ml | 26 ++++++ src/EverCrypt_DRBG.c | 16 ++-- src/Hacl_Ed25519.c | 33 ++++---- src/Hacl_Frodo1344.c | 48 +++++------ src/Hacl_Frodo64.c | 48 +++++------ src/Hacl_Frodo640.c | 48 +++++------ src/Hacl_Frodo976.c | 48 +++++------ src/Hacl_Hash_Blake2b.c | 80 +++++++++++++++--- src/Hacl_Hash_Blake2b_Simd256.c | 71 ++++++++++++++-- src/Hacl_Hash_Blake2s.c | 78 ++++++++++++++--- src/Hacl_Hash_Blake2s_Simd128.c | 68 +++++++++++++-- src/Hacl_K256_ECDSA.c | 4 - src/Lib_RandomBuffer_System.c | 1 + src/msvc/EverCrypt_DRBG.c | 16 ++-- src/msvc/Hacl_Ed25519.c | 33 ++++---- src/msvc/Hacl_Frodo1344.c | 48 +++++------ src/msvc/Hacl_Frodo64.c | 48 +++++------ src/msvc/Hacl_Frodo640.c | 48 +++++------ src/msvc/Hacl_Frodo976.c | 48 +++++------ src/msvc/Hacl_Hash_Blake2b.c | 80 +++++++++++++++--- src/msvc/Hacl_Hash_Blake2b_Simd256.c | 71 ++++++++++++++-- src/msvc/Hacl_Hash_Blake2s.c | 78 ++++++++++++++--- src/msvc/Hacl_Hash_Blake2s_Simd128.c | 68 +++++++++++++-- src/msvc/Hacl_K256_ECDSA.c | 4 - src/msvc/Lib_RandomBuffer_System.c | 1 + src/wasm/EverCrypt_Hash.wasm | Bin 49305 -> 48469 bytes .../Hacl_AEAD_Chacha20Poly1305_Simd256.wasm | Bin 1910 -> 1910 bytes src/wasm/Hacl_Ed25519_PrecompTable.wasm | Bin 16451 -> 16451 bytes src/wasm/Hacl_HMAC.wasm | Bin 29754 -> 28160 bytes src/wasm/Hacl_HMAC_DRBG.wasm | Bin 25396 -> 25396 bytes src/wasm/Hacl_Hash_Blake2b.wasm | Bin 15858 -> 16112 bytes src/wasm/Hacl_Hash_Blake2b_Simd256.wasm | Bin 6794 -> 7187 bytes src/wasm/Hacl_Hash_Blake2s.wasm | Bin 14005 -> 14330 bytes src/wasm/Hacl_Hash_Blake2s_Simd128.wasm | Bin 5638 -> 6030 bytes src/wasm/Hacl_K256_ECDSA.wasm | Bin 98188 -> 98133 bytes src/wasm/Hacl_SHA2_Vec128.wasm | Bin 5687 -> 5687 bytes src/wasm/INFO.txt | 4 +- src/wasm/layouts.json | 2 +- 50 files changed, 847 insertions(+), 377 deletions(-) diff --git a/include/Hacl_Ed25519.h b/include/Hacl_Ed25519.h index b2654704..f0dc31e2 100644 --- a/include/Hacl_Ed25519.h +++ b/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); diff --git a/include/internal/Hacl_Hash_Blake2b.h b/include/internal/Hacl_Hash_Blake2b.h index 21689d60..e2437d97 100644 --- a/include/internal/Hacl_Hash_Blake2b.h +++ b/include/internal/Hacl_Hash_Blake2b.h @@ -38,6 +38,21 @@ extern "C" { #include "internal/Hacl_Impl_Blake2_Constants.h" #include "../Hacl_Hash_Blake2b.h" +typedef struct Hacl_Hash_Blake2s_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_Blake2s_blake2_params; + void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn); void diff --git a/include/internal/Hacl_Hash_Blake2b_Simd256.h b/include/internal/Hacl_Hash_Blake2b_Simd256.h index 4cc07869..4dd986b2 100644 --- a/include/internal/Hacl_Hash_Blake2b_Simd256.h +++ b/include/internal/Hacl_Hash_Blake2b_Simd256.h @@ -36,6 +36,7 @@ extern "C" { #include "krml/internal/target.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2b_Simd256.h" #include "libintvector.h" diff --git a/include/internal/Hacl_Hash_Blake2s.h b/include/internal/Hacl_Hash_Blake2s.h index f814aa95..eccd92de 100644 --- a/include/internal/Hacl_Hash_Blake2s.h +++ b/include/internal/Hacl_Hash_Blake2s.h @@ -36,6 +36,7 @@ extern "C" { #include "krml/internal/target.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2s.h" void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn); diff --git a/include/internal/Hacl_Hash_Blake2s_Simd128.h b/include/internal/Hacl_Hash_Blake2s_Simd128.h index 0589aec5..2c422949 100644 --- a/include/internal/Hacl_Hash_Blake2s_Simd128.h +++ b/include/internal/Hacl_Hash_Blake2s_Simd128.h @@ -36,6 +36,7 @@ extern "C" { #include "krml/internal/target.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2s_Simd128.h" #include "libintvector.h" diff --git a/include/lib_memzero0.h b/include/lib_memzero0.h index 506dd50f..fea3e41c 100644 --- a/include/lib_memzero0.h +++ b/include/lib_memzero0.h @@ -2,4 +2,4 @@ void Lib_Memzero0_memzero0(void *dst, uint64_t len); -#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t)) +#define Lib_Memzero0_memzero(dst, len, t, _ret_t) Lib_Memzero0_memzero0(dst, len * sizeof(t)) diff --git a/include/msvc/Hacl_Ed25519.h b/include/msvc/Hacl_Ed25519.h index b2654704..f0dc31e2 100644 --- a/include/msvc/Hacl_Ed25519.h +++ b/include/msvc/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); diff --git a/include/msvc/internal/Hacl_Hash_Blake2b.h b/include/msvc/internal/Hacl_Hash_Blake2b.h index 21689d60..e2437d97 100644 --- a/include/msvc/internal/Hacl_Hash_Blake2b.h +++ b/include/msvc/internal/Hacl_Hash_Blake2b.h @@ -38,6 +38,21 @@ extern "C" { #include "internal/Hacl_Impl_Blake2_Constants.h" #include "../Hacl_Hash_Blake2b.h" +typedef struct Hacl_Hash_Blake2s_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_Blake2s_blake2_params; + void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn); void diff --git a/include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h b/include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h index 4cc07869..4dd986b2 100644 --- a/include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h +++ b/include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h @@ -36,6 +36,7 @@ extern "C" { #include "krml/internal/target.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2b_Simd256.h" #include "libintvector.h" diff --git a/include/msvc/internal/Hacl_Hash_Blake2s.h b/include/msvc/internal/Hacl_Hash_Blake2s.h index f814aa95..eccd92de 100644 --- a/include/msvc/internal/Hacl_Hash_Blake2s.h +++ b/include/msvc/internal/Hacl_Hash_Blake2s.h @@ -36,6 +36,7 @@ extern "C" { #include "krml/internal/target.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2s.h" void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn); diff --git a/include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h b/include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h index 0589aec5..2c422949 100644 --- a/include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h +++ b/include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h @@ -36,6 +36,7 @@ extern "C" { #include "krml/internal/target.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2s_Simd128.h" #include "libintvector.h" diff --git a/include/msvc/lib_memzero0.h b/include/msvc/lib_memzero0.h index 506dd50f..fea3e41c 100644 --- a/include/msvc/lib_memzero0.h +++ b/include/msvc/lib_memzero0.h @@ -2,4 +2,4 @@ void Lib_Memzero0_memzero0(void *dst, uint64_t len); -#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t)) +#define Lib_Memzero0_memzero(dst, len, t, _ret_t) Lib_Memzero0_memzero0(dst, len * sizeof(t)) diff --git a/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml b/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml index 75c75e90..b594e2ef 100644 --- a/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml +++ b/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml @@ -5,6 +5,32 @@ module Bindings(F:Cstubs.FOREIGN) = module Hacl_Streaming_Types_applied = (Hacl_Streaming_Types_bindings.Bindings)(Hacl_Streaming_Types_stubs) open Hacl_Streaming_Types_applied + type hacl_Hash_Blake2s_blake2_params = + [ `hacl_Hash_Blake2s_blake2_params ] structure + let (hacl_Hash_Blake2s_blake2_params : + [ `hacl_Hash_Blake2s_blake2_params ] structure typ) = + structure "Hacl_Hash_Blake2s_blake2_params_s" + let hacl_Hash_Blake2s_blake2_params_digest_length = + field hacl_Hash_Blake2s_blake2_params "digest_length" uint8_t + let hacl_Hash_Blake2s_blake2_params_key_length = + field hacl_Hash_Blake2s_blake2_params "key_length" uint8_t + let hacl_Hash_Blake2s_blake2_params_fanout = + field hacl_Hash_Blake2s_blake2_params "fanout" uint8_t + let hacl_Hash_Blake2s_blake2_params_depth = + field hacl_Hash_Blake2s_blake2_params "depth" uint8_t + let hacl_Hash_Blake2s_blake2_params_leaf_length = + field hacl_Hash_Blake2s_blake2_params "leaf_length" uint32_t + let hacl_Hash_Blake2s_blake2_params_node_offset = + field hacl_Hash_Blake2s_blake2_params "node_offset" uint64_t + let hacl_Hash_Blake2s_blake2_params_node_depth = + field hacl_Hash_Blake2s_blake2_params "node_depth" uint8_t + let hacl_Hash_Blake2s_blake2_params_inner_length = + field hacl_Hash_Blake2s_blake2_params "inner_length" uint8_t + let hacl_Hash_Blake2s_blake2_params_salt = + field hacl_Hash_Blake2s_blake2_params "salt" (ptr uint8_t) + let hacl_Hash_Blake2s_blake2_params_personal = + field hacl_Hash_Blake2s_blake2_params "personal" (ptr uint8_t) + let _ = seal hacl_Hash_Blake2s_blake2_params let hacl_Hash_Blake2b_init = foreign "Hacl_Hash_Blake2b_init" ((ptr uint64_t) @-> (uint32_t @-> (uint32_t @-> (returning void)))) diff --git a/src/EverCrypt_DRBG.c b/src/EverCrypt_DRBG.c index 301fe528..a831a5b5 100644 --- a/src/EverCrypt_DRBG.c +++ b/src/EverCrypt_DRBG.c @@ -1770,8 +1770,8 @@ static void uninstantiate_sha1(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 20U, uint8_t); - Lib_Memzero0_memzero(v, 20U, uint8_t); + Lib_Memzero0_memzero(k, 20U, uint8_t, void *); + Lib_Memzero0_memzero(v, 20U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); @@ -1794,8 +1794,8 @@ static void uninstantiate_sha2_256(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 32U, uint8_t); - Lib_Memzero0_memzero(v, 32U, uint8_t); + Lib_Memzero0_memzero(k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(v, 32U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); @@ -1818,8 +1818,8 @@ static void uninstantiate_sha2_384(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 48U, uint8_t); - Lib_Memzero0_memzero(v, 48U, uint8_t); + Lib_Memzero0_memzero(k, 48U, uint8_t, void *); + Lib_Memzero0_memzero(v, 48U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); @@ -1842,8 +1842,8 @@ static void uninstantiate_sha2_512(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 64U, uint8_t); - Lib_Memzero0_memzero(v, 64U, uint8_t); + Lib_Memzero0_memzero(k, 64U, uint8_t, void *); + Lib_Memzero0_memzero(v, 64U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); diff --git a/src/Hacl_Ed25519.c b/src/Hacl_Ed25519.c index 05d96cd0..d1f8edf2 100644 --- a/src/Hacl_Ed25519.c +++ b/src/Hacl_Ed25519.c @@ -1712,8 +1712,8 @@ static inline void secret_expand(uint8_t *expanded, uint8_t *secret) /** 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) { @@ -1726,8 +1726,8 @@ 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. @@ -1744,11 +1744,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. @@ -1783,9 +1782,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`. @@ -1803,11 +1803,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) diff --git a/src/Hacl_Frodo1344.c b/src/Hacl_Frodo1344.c index a565a85b..741a593b 100644 --- a/src/Hacl_Frodo1344.c +++ b/src/Hacl_Frodo1344.c @@ -55,7 +55,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43008U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(1344U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(1344U, 8U, r + 21504U, e_matrix); uint16_t b_matrix[10752U] = { 0U }; @@ -66,14 +66,14 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(1344U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(1344U, 8U, 16U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(1344U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 10752U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 10752U, uint16_t, void *); uint32_t slen1 = 43056U; uint8_t *sk_p = sk; memcpy(sk_p, s, 32U * sizeof (uint8_t)); memcpy(sk_p + 32U, pk, 21520U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(21520U, pk, 32U, sk + slen1); - Lib_Memzero0_memzero(coins, 80U, uint8_t); + Lib_Memzero0_memzero(coins, 80U, uint8_t, void *); return 0U; } @@ -98,7 +98,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43136U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r + 21504U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 8U, r + 43008U, epp_matrix); @@ -119,12 +119,12 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 4U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 16U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 21664U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t shake_input_ss[ss_init_len]; @@ -132,9 +132,9 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 21632U * sizeof (uint8_t)); memcpy(shake_input_ss + 21632U, k, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, shake_input_ss, 32U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t); - Lib_Memzero0_memzero(coins, 32U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 32U, uint8_t, void *); return 0U; } @@ -154,8 +154,8 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 1344U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(16U, 4U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[64U] = { 0U }; uint32_t pkh_mu_decode_len = 64U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -178,7 +178,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43136U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r + 21504U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 8U, r + 43008U, epp_matrix); @@ -197,12 +197,12 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 4U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 1344U, 16U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 16U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 1344U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -223,10 +223,10 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 21632U * sizeof (uint8_t)); memcpy(ss_init + 21632U, kp_s, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, ss_init, 32U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 32U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 32U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 32U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 32U, uint8_t, void *); return 0U; } diff --git a/src/Hacl_Frodo64.c b/src/Hacl_Frodo64.c index 91434038..b54a7c62 100644 --- a/src/Hacl_Frodo64.c +++ b/src/Hacl_Frodo64.c @@ -60,7 +60,7 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2048U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r + 1024U, e_matrix); uint16_t b_matrix[512U] = { 0U }; @@ -70,14 +70,14 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(64U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(64U, 8U, 15U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(64U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 512U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 512U, uint16_t, void *); uint32_t slen1 = 2016U; uint8_t *sk_p = sk; memcpy(sk_p, s, 16U * sizeof (uint8_t)); memcpy(sk_p + 16U, pk, 976U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(976U, pk, 16U, sk + slen1); - Lib_Memzero0_memzero(coins, 48U, uint8_t); + Lib_Memzero0_memzero(coins, 48U, uint8_t, void *); return 0U; } @@ -102,7 +102,7 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix); @@ -122,12 +122,12 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 15U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 1096U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t shake_input_ss[ss_init_len]; @@ -135,9 +135,9 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 1080U * sizeof (uint8_t)); memcpy(shake_input_ss + 1080U, k, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(coins, 16U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 16U, uint8_t, void *); return 0U; } @@ -157,8 +157,8 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 64U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(15U, 2U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[32U] = { 0U }; uint32_t pkh_mu_decode_len = 32U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -181,7 +181,7 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix); @@ -199,12 +199,12 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 64U, 15U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 64U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -226,10 +226,10 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 1080U * sizeof (uint8_t)); memcpy(ss_init + 1080U, kp_s, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 16U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 16U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *); return 0U; } diff --git a/src/Hacl_Frodo640.c b/src/Hacl_Frodo640.c index 8baaee46..86f3ed23 100644 --- a/src/Hacl_Frodo640.c +++ b/src/Hacl_Frodo640.c @@ -55,7 +55,7 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20480U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r + 10240U, e_matrix); uint16_t b_matrix[5120U] = { 0U }; @@ -66,14 +66,14 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(640U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(640U, 8U, 15U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(640U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t, void *); uint32_t slen1 = 19872U; uint8_t *sk_p = sk; memcpy(sk_p, s, 16U * sizeof (uint8_t)); memcpy(sk_p + 16U, pk, 9616U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(9616U, pk, 16U, sk + slen1); - Lib_Memzero0_memzero(coins, 48U, uint8_t); + Lib_Memzero0_memzero(coins, 48U, uint8_t, void *); return 0U; } @@ -98,7 +98,7 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix); @@ -119,12 +119,12 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 15U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 9736U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t shake_input_ss[ss_init_len]; @@ -132,9 +132,9 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 9720U * sizeof (uint8_t)); memcpy(shake_input_ss + 9720U, k, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(coins, 16U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 16U, uint8_t, void *); return 0U; } @@ -154,8 +154,8 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 640U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(15U, 2U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[32U] = { 0U }; uint32_t pkh_mu_decode_len = 32U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -178,7 +178,7 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix); @@ -197,12 +197,12 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 640U, 15U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 640U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -224,10 +224,10 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 9720U * sizeof (uint8_t)); memcpy(ss_init + 9720U, kp_s, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 16U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 16U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *); return 0U; } diff --git a/src/Hacl_Frodo976.c b/src/Hacl_Frodo976.c index 76d78a30..3e3dca8e 100644 --- a/src/Hacl_Frodo976.c +++ b/src/Hacl_Frodo976.c @@ -55,7 +55,7 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31232U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r + 15616U, e_matrix); uint16_t b_matrix[7808U] = { 0U }; @@ -66,14 +66,14 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(976U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(976U, 8U, 16U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(976U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t, void *); uint32_t slen1 = 31272U; uint8_t *sk_p = sk; memcpy(sk_p, s, 24U * sizeof (uint8_t)); memcpy(sk_p + 24U, pk, 15632U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(15632U, pk, 24U, sk + slen1); - Lib_Memzero0_memzero(coins, 64U, uint8_t); + Lib_Memzero0_memzero(coins, 64U, uint8_t, void *); return 0U; } @@ -98,7 +98,7 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix); @@ -119,12 +119,12 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 3U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 16U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 15768U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t shake_input_ss[ss_init_len]; @@ -132,9 +132,9 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 15744U * sizeof (uint8_t)); memcpy(shake_input_ss + 15744U, k, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, shake_input_ss, 24U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t); - Lib_Memzero0_memzero(coins, 24U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 24U, uint8_t, void *); return 0U; } @@ -154,8 +154,8 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 976U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(16U, 3U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[48U] = { 0U }; uint32_t pkh_mu_decode_len = 48U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -178,7 +178,7 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix); @@ -197,12 +197,12 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 3U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 976U, 16U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 16U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 976U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -223,10 +223,10 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 15744U * sizeof (uint8_t)); memcpy(ss_init + 15744U, kp_s, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, ss_init, 24U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 24U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 24U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 24U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 24U, uint8_t, void *); return 0U; } diff --git a/src/Hacl_Hash_Blake2b.c b/src/Hacl_Hash_Blake2b.c index 2dceaf4b..68de8340 100644 --- a/src/Hacl_Hash_Blake2b.c +++ b/src/Hacl_Hash_Blake2b.c @@ -474,6 +474,7 @@ update_block(uint64_t *wv, uint64_t *hash, bool flag, FStar_UInt128_uint128 totl void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn) { + uint64_t tmp[8U] = { 0U }; uint64_t *r0 = hash; uint64_t *r1 = hash + 4U; uint64_t *r2 = hash + 8U; @@ -494,16 +495,67 @@ void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn) r3[1U] = iv5; r3[2U] = iv6; r3[3U] = iv7; - uint64_t kk_shift_8 = (uint64_t)kk << 8U; - uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn)); + uint8_t salt[16U] = { 0U }; + uint8_t personal[16U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + tmp[0U] = + (uint64_t)nn + ^ + ((uint64_t)kk + << 8U + ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U))); + tmp[1U] = p.node_offset; + tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U; + tmp[3U] = 0ULL; + uint64_t tmp0 = tmp[0U]; + uint64_t tmp1 = tmp[1U]; + uint64_t tmp2 = tmp[2U]; + uint64_t tmp3 = tmp[3U]; + uint64_t tmp4 = tmp[4U]; + uint64_t tmp5 = tmp[5U]; + uint64_t tmp6 = tmp[6U]; + uint64_t tmp7 = tmp[7U]; + uint64_t iv0_ = iv0 ^ tmp0; + uint64_t iv1_ = iv1 ^ tmp1; + uint64_t iv2_ = iv2 ^ tmp2; + uint64_t iv3_ = iv3 ^ tmp3; + uint64_t iv4_ = iv4 ^ tmp4; + uint64_t iv5_ = iv5 ^ tmp5; + uint64_t iv6_ = iv6 ^ tmp6; + uint64_t iv7_ = iv7 ^ tmp7; r0[0U] = iv0_; - r0[1U] = iv1; - r0[2U] = iv2; - r0[3U] = iv3; - r1[0U] = iv4; - r1[1U] = iv5; - r1[2U] = iv6; - r1[3U] = iv7; + r0[1U] = iv1_; + r0[2U] = iv2_; + r0[3U] = iv3_; + r1[0U] = iv4_; + r1[1U] = iv5_; + r1[2U] = iv6_; + r1[3U] = iv7_; } static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, uint32_t ll) @@ -519,7 +571,7 @@ static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, ui { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } void @@ -560,7 +612,7 @@ Hacl_Hash_Blake2b_update_last( FStar_UInt128_uint128 totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len)); update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } static void @@ -624,7 +676,7 @@ void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash) KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store64_le(second + i * 8U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } /** @@ -965,7 +1017,7 @@ Hacl_Hash_Blake2b_hash_with_key( Hacl_Hash_Blake2b_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2b_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 16U, uint64_t); - Lib_Memzero0_memzero(b, 16U, uint64_t); + Lib_Memzero0_memzero(b1, 16U, uint64_t, void *); + Lib_Memzero0_memzero(b, 16U, uint64_t, void *); } diff --git a/src/Hacl_Hash_Blake2b_Simd256.c b/src/Hacl_Hash_Blake2b_Simd256.c index 1a5e8cf2..7aea4d42 100644 --- a/src/Hacl_Hash_Blake2b_Simd256.c +++ b/src/Hacl_Hash_Blake2b_Simd256.c @@ -26,6 +26,7 @@ #include "internal/Hacl_Hash_Blake2b_Simd256.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" static inline void @@ -214,6 +215,7 @@ update_block( void Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t kk, uint32_t nn) { + uint64_t tmp[8U] = { 0U }; Lib_IntVector_Intrinsics_vec256 *r0 = hash; Lib_IntVector_Intrinsics_vec256 *r1 = hash + 1U; Lib_IntVector_Intrinsics_vec256 *r2 = hash + 2U; @@ -228,10 +230,61 @@ Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t k uint64_t iv7 = Hacl_Hash_Blake2s_ivTable_B[7U]; r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3); r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7); - uint64_t kk_shift_8 = (uint64_t)kk << 8U; - uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn)); - r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1, iv2, iv3); - r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7); + uint8_t salt[16U] = { 0U }; + uint8_t personal[16U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + tmp[0U] = + (uint64_t)nn + ^ + ((uint64_t)kk + << 8U + ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U))); + tmp[1U] = p.node_offset; + tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U; + tmp[3U] = 0ULL; + uint64_t tmp0 = tmp[0U]; + uint64_t tmp1 = tmp[1U]; + uint64_t tmp2 = tmp[2U]; + uint64_t tmp3 = tmp[3U]; + uint64_t tmp4 = tmp[4U]; + uint64_t tmp5 = tmp[5U]; + uint64_t tmp6 = tmp[6U]; + uint64_t tmp7 = tmp[7U]; + uint64_t iv0_ = iv0 ^ tmp0; + uint64_t iv1_ = iv1 ^ tmp1; + uint64_t iv2_ = iv2 ^ tmp2; + uint64_t iv3_ = iv3 ^ tmp3; + uint64_t iv4_ = iv4 ^ tmp4; + uint64_t iv5_ = iv5 ^ tmp5; + uint64_t iv6_ = iv6 ^ tmp6; + uint64_t iv7_ = iv7 ^ tmp7; + r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_); + r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_); } static void @@ -254,7 +307,7 @@ update_key( { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } void @@ -295,7 +348,7 @@ Hacl_Hash_Blake2b_Simd256_update_last( FStar_UInt128_uint128 totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len)); update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } static inline void @@ -371,7 +424,7 @@ Hacl_Hash_Blake2b_Simd256_finish( Lib_IntVector_Intrinsics_vec256_store64_le(second, row1[0U]); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } void @@ -822,7 +875,7 @@ Hacl_Hash_Blake2b_Simd256_hash_with_key( Hacl_Hash_Blake2b_Simd256_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2b_Simd256_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256); - Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256); + Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256, void *); + Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256, void *); } diff --git a/src/Hacl_Hash_Blake2s.c b/src/Hacl_Hash_Blake2s.c index 652c3f33..37fabb67 100644 --- a/src/Hacl_Hash_Blake2s.c +++ b/src/Hacl_Hash_Blake2s.c @@ -26,6 +26,7 @@ #include "internal/Hacl_Hash_Blake2s.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" static inline void @@ -474,6 +475,7 @@ update_block(uint32_t *wv, uint32_t *hash, bool flag, uint64_t totlen, uint8_t * void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn) { + uint32_t tmp[8U] = { 0U }; uint32_t *r0 = hash; uint32_t *r1 = hash + 4U; uint32_t *r2 = hash + 8U; @@ -494,16 +496,64 @@ void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn) r3[1U] = iv5; r3[2U] = iv6; r3[3U] = iv7; - uint32_t kk_shift_8 = kk << 8U; - uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn)); + uint8_t salt[8U] = { 0U }; + uint8_t personal[8U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U)); + tmp[1U] = p.leaf_length; + tmp[2U] = (uint32_t)p.node_offset; + tmp[3U] = + (uint32_t)(p.node_offset >> 32U) + ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U); + uint32_t tmp0 = tmp[0U]; + uint32_t tmp1 = tmp[1U]; + uint32_t tmp2 = tmp[2U]; + uint32_t tmp3 = tmp[3U]; + uint32_t tmp4 = tmp[4U]; + uint32_t tmp5 = tmp[5U]; + uint32_t tmp6 = tmp[6U]; + uint32_t tmp7 = tmp[7U]; + uint32_t iv0_ = iv0 ^ tmp0; + uint32_t iv1_ = iv1 ^ tmp1; + uint32_t iv2_ = iv2 ^ tmp2; + uint32_t iv3_ = iv3 ^ tmp3; + uint32_t iv4_ = iv4 ^ tmp4; + uint32_t iv5_ = iv5 ^ tmp5; + uint32_t iv6_ = iv6 ^ tmp6; + uint32_t iv7_ = iv7 ^ tmp7; r0[0U] = iv0_; - r0[1U] = iv1; - r0[2U] = iv2; - r0[3U] = iv3; - r1[0U] = iv4; - r1[1U] = iv5; - r1[2U] = iv6; - r1[3U] = iv7; + r0[1U] = iv1_; + r0[2U] = iv2_; + r0[3U] = iv3_; + r1[0U] = iv4_; + r1[1U] = iv5_; + r1[2U] = iv6_; + r1[3U] = iv7_; } static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, uint32_t ll) @@ -519,7 +569,7 @@ static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, ui { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } void @@ -556,7 +606,7 @@ Hacl_Hash_Blake2s_update_last( memcpy(b, last, rem * sizeof (uint8_t)); uint64_t totlen = prev + (uint64_t)len; update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } static void @@ -614,7 +664,7 @@ void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash) KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store32_le(second + i * 4U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 32U, uint8_t); + Lib_Memzero0_memzero(b, 32U, uint8_t, void *); } /** @@ -925,7 +975,7 @@ Hacl_Hash_Blake2s_hash_with_key( Hacl_Hash_Blake2s_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2s_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 16U, uint32_t); - Lib_Memzero0_memzero(b, 16U, uint32_t); + Lib_Memzero0_memzero(b1, 16U, uint32_t, void *); + Lib_Memzero0_memzero(b, 16U, uint32_t, void *); } diff --git a/src/Hacl_Hash_Blake2s_Simd128.c b/src/Hacl_Hash_Blake2s_Simd128.c index 73f0cccb..ed86be43 100644 --- a/src/Hacl_Hash_Blake2s_Simd128.c +++ b/src/Hacl_Hash_Blake2s_Simd128.c @@ -26,6 +26,7 @@ #include "internal/Hacl_Hash_Blake2s_Simd128.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" static inline void @@ -214,6 +215,7 @@ update_block( void Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t kk, uint32_t nn) { + uint32_t tmp[8U] = { 0U }; Lib_IntVector_Intrinsics_vec128 *r0 = hash; Lib_IntVector_Intrinsics_vec128 *r1 = hash + 1U; Lib_IntVector_Intrinsics_vec128 *r2 = hash + 2U; @@ -228,10 +230,58 @@ Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t k uint32_t iv7 = Hacl_Hash_Blake2s_ivTable_S[7U]; r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3); r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7); - uint32_t kk_shift_8 = kk << 8U; - uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn)); - r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1, iv2, iv3); - r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7); + uint8_t salt[8U] = { 0U }; + uint8_t personal[8U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U)); + tmp[1U] = p.leaf_length; + tmp[2U] = (uint32_t)p.node_offset; + tmp[3U] = + (uint32_t)(p.node_offset >> 32U) + ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U); + uint32_t tmp0 = tmp[0U]; + uint32_t tmp1 = tmp[1U]; + uint32_t tmp2 = tmp[2U]; + uint32_t tmp3 = tmp[3U]; + uint32_t tmp4 = tmp[4U]; + uint32_t tmp5 = tmp[5U]; + uint32_t tmp6 = tmp[6U]; + uint32_t tmp7 = tmp[7U]; + uint32_t iv0_ = iv0 ^ tmp0; + uint32_t iv1_ = iv1 ^ tmp1; + uint32_t iv2_ = iv2 ^ tmp2; + uint32_t iv3_ = iv3 ^ tmp3; + uint32_t iv4_ = iv4 ^ tmp4; + uint32_t iv5_ = iv5 ^ tmp5; + uint32_t iv6_ = iv6 ^ tmp6; + uint32_t iv7_ = iv7 ^ tmp7; + r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_); + r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_); } static void @@ -254,7 +304,7 @@ update_key( { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } void @@ -291,7 +341,7 @@ Hacl_Hash_Blake2s_Simd128_update_last( memcpy(b, last, rem * sizeof (uint8_t)); uint64_t totlen = prev + (uint64_t)len; update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } static inline void @@ -367,7 +417,7 @@ Hacl_Hash_Blake2s_Simd128_finish( Lib_IntVector_Intrinsics_vec128_store32_le(second, row1[0U]); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 32U, uint8_t); + Lib_Memzero0_memzero(b, 32U, uint8_t, void *); } void @@ -788,7 +838,7 @@ Hacl_Hash_Blake2s_Simd128_hash_with_key( Hacl_Hash_Blake2s_Simd128_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2s_Simd128_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128); - Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128); + Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128, void *); + Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128, void *); } diff --git a/src/Hacl_K256_ECDSA.c b/src/Hacl_K256_ECDSA.c index bbd2c615..0b72b166 100644 --- a/src/Hacl_K256_ECDSA.c +++ b/src/Hacl_K256_ECDSA.c @@ -571,10 +571,6 @@ static inline bool is_qelem_le_q_halved_vartime(uint64_t *f) { return true; } - if (a2 > 0xffffffffffffffffULL) - { - return false; - } if (a1 < 0x5d576e7357a4501dULL) { return true; diff --git a/src/Lib_RandomBuffer_System.c b/src/Lib_RandomBuffer_System.c index 0d7924b4..de6ef337 100644 --- a/src/Lib_RandomBuffer_System.c +++ b/src/Lib_RandomBuffer_System.c @@ -31,6 +31,7 @@ bool read_random_bytes(uint32_t len, uint8_t *buf) { #include #include #include +#include #include bool read_random_bytes(uint32_t len, uint8_t *buf) { diff --git a/src/msvc/EverCrypt_DRBG.c b/src/msvc/EverCrypt_DRBG.c index 1395f59f..c76a69cd 100644 --- a/src/msvc/EverCrypt_DRBG.c +++ b/src/msvc/EverCrypt_DRBG.c @@ -1798,8 +1798,8 @@ static void uninstantiate_sha1(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 20U, uint8_t); - Lib_Memzero0_memzero(v, 20U, uint8_t); + Lib_Memzero0_memzero(k, 20U, uint8_t, void *); + Lib_Memzero0_memzero(v, 20U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); @@ -1822,8 +1822,8 @@ static void uninstantiate_sha2_256(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 32U, uint8_t); - Lib_Memzero0_memzero(v, 32U, uint8_t); + Lib_Memzero0_memzero(k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(v, 32U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); @@ -1846,8 +1846,8 @@ static void uninstantiate_sha2_384(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 48U, uint8_t); - Lib_Memzero0_memzero(v, 48U, uint8_t); + Lib_Memzero0_memzero(k, 48U, uint8_t, void *); + Lib_Memzero0_memzero(v, 48U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); @@ -1870,8 +1870,8 @@ static void uninstantiate_sha2_512(EverCrypt_DRBG_state_s *st) uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; - Lib_Memzero0_memzero(k, 64U, uint8_t); - Lib_Memzero0_memzero(v, 64U, uint8_t); + Lib_Memzero0_memzero(k, 64U, uint8_t, void *); + Lib_Memzero0_memzero(v, 64U, uint8_t, void *); ctr[0U] = 0U; KRML_HOST_FREE(k); KRML_HOST_FREE(v); diff --git a/src/msvc/Hacl_Ed25519.c b/src/msvc/Hacl_Ed25519.c index 05d96cd0..d1f8edf2 100644 --- a/src/msvc/Hacl_Ed25519.c +++ b/src/msvc/Hacl_Ed25519.c @@ -1712,8 +1712,8 @@ static inline void secret_expand(uint8_t *expanded, uint8_t *secret) /** 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) { @@ -1726,8 +1726,8 @@ 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. @@ -1744,11 +1744,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. @@ -1783,9 +1782,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`. @@ -1803,11 +1803,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) diff --git a/src/msvc/Hacl_Frodo1344.c b/src/msvc/Hacl_Frodo1344.c index 61262a4c..f4c19de3 100644 --- a/src/msvc/Hacl_Frodo1344.c +++ b/src/msvc/Hacl_Frodo1344.c @@ -55,7 +55,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43008U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(1344U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(1344U, 8U, r + 21504U, e_matrix); uint16_t b_matrix[10752U] = { 0U }; @@ -66,14 +66,14 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(1344U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(1344U, 8U, 16U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(1344U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 10752U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 10752U, uint16_t, void *); uint32_t slen1 = 43056U; uint8_t *sk_p = sk; memcpy(sk_p, s, 32U * sizeof (uint8_t)); memcpy(sk_p + 32U, pk, 21520U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(21520U, pk, 32U, sk + slen1); - Lib_Memzero0_memzero(coins, 80U, uint8_t); + Lib_Memzero0_memzero(coins, 80U, uint8_t, void *); return 0U; } @@ -98,7 +98,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43136U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r + 21504U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 8U, r + 43008U, epp_matrix); @@ -119,12 +119,12 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 4U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 16U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 21664U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t *shake_input_ss = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t)); @@ -132,9 +132,9 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 21632U * sizeof (uint8_t)); memcpy(shake_input_ss + 21632U, k, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, shake_input_ss, 32U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t); - Lib_Memzero0_memzero(coins, 32U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 32U, uint8_t, void *); return 0U; } @@ -154,8 +154,8 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 1344U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(16U, 4U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[64U] = { 0U }; uint32_t pkh_mu_decode_len = 64U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -178,7 +178,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43136U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r + 21504U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 8U, r + 43008U, epp_matrix); @@ -197,12 +197,12 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 4U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 1344U, 16U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 16U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 1344U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -223,10 +223,10 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 21632U * sizeof (uint8_t)); memcpy(ss_init + 21632U, kp_s, 32U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, ss_init, 32U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 32U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 32U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 32U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 32U, uint8_t, void *); return 0U; } diff --git a/src/msvc/Hacl_Frodo64.c b/src/msvc/Hacl_Frodo64.c index 392d87f9..e9a19d93 100644 --- a/src/msvc/Hacl_Frodo64.c +++ b/src/msvc/Hacl_Frodo64.c @@ -60,7 +60,7 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2048U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r + 1024U, e_matrix); uint16_t b_matrix[512U] = { 0U }; @@ -70,14 +70,14 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(64U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(64U, 8U, 15U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(64U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 512U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 512U, uint16_t, void *); uint32_t slen1 = 2016U; uint8_t *sk_p = sk; memcpy(sk_p, s, 16U * sizeof (uint8_t)); memcpy(sk_p + 16U, pk, 976U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(976U, pk, 16U, sk + slen1); - Lib_Memzero0_memzero(coins, 48U, uint8_t); + Lib_Memzero0_memzero(coins, 48U, uint8_t, void *); return 0U; } @@ -102,7 +102,7 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix); @@ -122,12 +122,12 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 15U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 1096U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t *shake_input_ss = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t)); @@ -135,9 +135,9 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 1080U * sizeof (uint8_t)); memcpy(shake_input_ss + 1080U, k, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(coins, 16U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 16U, uint8_t, void *); return 0U; } @@ -157,8 +157,8 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 64U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(15U, 2U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[32U] = { 0U }; uint32_t pkh_mu_decode_len = 32U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -181,7 +181,7 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix); @@ -199,12 +199,12 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 64U, 15U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 64U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -226,10 +226,10 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 1080U * sizeof (uint8_t)); memcpy(ss_init + 1080U, kp_s, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 16U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 16U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *); return 0U; } diff --git a/src/msvc/Hacl_Frodo640.c b/src/msvc/Hacl_Frodo640.c index 5de5871f..3a117991 100644 --- a/src/msvc/Hacl_Frodo640.c +++ b/src/msvc/Hacl_Frodo640.c @@ -55,7 +55,7 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20480U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r + 10240U, e_matrix); uint16_t b_matrix[5120U] = { 0U }; @@ -66,14 +66,14 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(640U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(640U, 8U, 15U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(640U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t, void *); uint32_t slen1 = 19872U; uint8_t *sk_p = sk; memcpy(sk_p, s, 16U * sizeof (uint8_t)); memcpy(sk_p + 16U, pk, 9616U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(9616U, pk, 16U, sk + slen1); - Lib_Memzero0_memzero(coins, 48U, uint8_t); + Lib_Memzero0_memzero(coins, 48U, uint8_t, void *); return 0U; } @@ -98,7 +98,7 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix); @@ -119,12 +119,12 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 15U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 9736U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t *shake_input_ss = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t)); @@ -132,9 +132,9 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 9720U * sizeof (uint8_t)); memcpy(shake_input_ss + 9720U, k, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(coins, 16U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 16U, uint8_t, void *); return 0U; } @@ -154,8 +154,8 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 640U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(15U, 2U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[32U] = { 0U }; uint32_t pkh_mu_decode_len = 32U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -178,7 +178,7 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix); @@ -197,12 +197,12 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(15U, 2U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 640U, 15U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 640U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -224,10 +224,10 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 9720U * sizeof (uint8_t)); memcpy(ss_init + 9720U, kp_s, 16U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 16U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 16U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *); return 0U; } diff --git a/src/msvc/Hacl_Frodo976.c b/src/msvc/Hacl_Frodo976.c index 61454ceb..b358a5e2 100644 --- a/src/msvc/Hacl_Frodo976.c +++ b/src/msvc/Hacl_Frodo976.c @@ -55,7 +55,7 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) shake_input_seed_se[0U] = 0x5fU; memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31232U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r, s_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r + 15616U, e_matrix); uint16_t b_matrix[7808U] = { 0U }; @@ -66,14 +66,14 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk) Hacl_Impl_Matrix_matrix_add(976U, 8U, b_matrix, e_matrix); Hacl_Impl_Frodo_Pack_frodo_pack(976U, 8U, 16U, b_matrix, b_bytes); Hacl_Impl_Matrix_matrix_to_lbytes(976U, 8U, s_matrix, s_bytes); - Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t, void *); uint32_t slen1 = 31272U; uint8_t *sk_p = sk; memcpy(sk_p, s, 24U * sizeof (uint8_t)); memcpy(sk_p + 24U, pk, 15632U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(15632U, pk, 24U, sk + slen1); - Lib_Memzero0_memzero(coins, 64U, uint8_t); + Lib_Memzero0_memzero(coins, 64U, uint8_t, void *); return 0U; } @@ -98,7 +98,7 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix); @@ -119,12 +119,12 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 3U, 8U, coins, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 16U, v_matrix, c2); - Lib_Memzero0_memzero(v_matrix, 64U, uint16_t); - Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *); + Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint32_t ss_init_len = 15768U; KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len); uint8_t *shake_input_ss = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t)); @@ -132,9 +132,9 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk) memcpy(shake_input_ss, ct, 15744U * sizeof (uint8_t)); memcpy(shake_input_ss + 15744U, k, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, shake_input_ss, 24U, ss); - Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t); - Lib_Memzero0_memzero(coins, 24U, uint8_t); + Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *); + Lib_Memzero0_memzero(coins, 24U, uint8_t, void *); return 0U; } @@ -154,8 +154,8 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) Hacl_Impl_Matrix_matrix_mul_s(8U, 976U, 8U, bp_matrix, s_matrix, m_matrix); Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix); Hacl_Impl_Frodo_Encode_frodo_key_decode(16U, 3U, 8U, m_matrix, mu_decode); - Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(m_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *); uint8_t seed_se_k[48U] = { 0U }; uint32_t pkh_mu_decode_len = 48U; KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len); @@ -178,7 +178,7 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) shake_input_seed_se[0U] = 0x96U; memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r); - Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t); + Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix); Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix); @@ -197,12 +197,12 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) uint16_t mu_encode[64U] = { 0U }; Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 3U, 8U, mu_decode, mu_encode); Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode); - Lib_Memzero0_memzero(mu_encode, 64U, uint16_t); + Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *); Hacl_Impl_Matrix_mod_pow2(8U, 976U, 16U, bpp_matrix); Hacl_Impl_Matrix_mod_pow2(8U, 8U, 16U, cp_matrix); - Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t); - Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t); + Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *); + Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *); uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 976U, bp_matrix, bpp_matrix); uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix); uint16_t mask = (uint32_t)b1 & (uint32_t)b2; @@ -223,10 +223,10 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk) memcpy(ss_init, ct, 15744U * sizeof (uint8_t)); memcpy(ss_init + 15744U, kp_s, 24U * sizeof (uint8_t)); Hacl_Hash_SHA3_shake256_hacl(ss_init_len, ss_init, 24U, ss); - Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t); - Lib_Memzero0_memzero(kp_s, 24U, uint8_t); - Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t); - Lib_Memzero0_memzero(mu_decode, 24U, uint8_t); + Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *); + Lib_Memzero0_memzero(kp_s, 24U, uint8_t, void *); + Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *); + Lib_Memzero0_memzero(mu_decode, 24U, uint8_t, void *); return 0U; } diff --git a/src/msvc/Hacl_Hash_Blake2b.c b/src/msvc/Hacl_Hash_Blake2b.c index 2dceaf4b..68de8340 100644 --- a/src/msvc/Hacl_Hash_Blake2b.c +++ b/src/msvc/Hacl_Hash_Blake2b.c @@ -474,6 +474,7 @@ update_block(uint64_t *wv, uint64_t *hash, bool flag, FStar_UInt128_uint128 totl void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn) { + uint64_t tmp[8U] = { 0U }; uint64_t *r0 = hash; uint64_t *r1 = hash + 4U; uint64_t *r2 = hash + 8U; @@ -494,16 +495,67 @@ void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn) r3[1U] = iv5; r3[2U] = iv6; r3[3U] = iv7; - uint64_t kk_shift_8 = (uint64_t)kk << 8U; - uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn)); + uint8_t salt[16U] = { 0U }; + uint8_t personal[16U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + tmp[0U] = + (uint64_t)nn + ^ + ((uint64_t)kk + << 8U + ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U))); + tmp[1U] = p.node_offset; + tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U; + tmp[3U] = 0ULL; + uint64_t tmp0 = tmp[0U]; + uint64_t tmp1 = tmp[1U]; + uint64_t tmp2 = tmp[2U]; + uint64_t tmp3 = tmp[3U]; + uint64_t tmp4 = tmp[4U]; + uint64_t tmp5 = tmp[5U]; + uint64_t tmp6 = tmp[6U]; + uint64_t tmp7 = tmp[7U]; + uint64_t iv0_ = iv0 ^ tmp0; + uint64_t iv1_ = iv1 ^ tmp1; + uint64_t iv2_ = iv2 ^ tmp2; + uint64_t iv3_ = iv3 ^ tmp3; + uint64_t iv4_ = iv4 ^ tmp4; + uint64_t iv5_ = iv5 ^ tmp5; + uint64_t iv6_ = iv6 ^ tmp6; + uint64_t iv7_ = iv7 ^ tmp7; r0[0U] = iv0_; - r0[1U] = iv1; - r0[2U] = iv2; - r0[3U] = iv3; - r1[0U] = iv4; - r1[1U] = iv5; - r1[2U] = iv6; - r1[3U] = iv7; + r0[1U] = iv1_; + r0[2U] = iv2_; + r0[3U] = iv3_; + r1[0U] = iv4_; + r1[1U] = iv5_; + r1[2U] = iv6_; + r1[3U] = iv7_; } static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, uint32_t ll) @@ -519,7 +571,7 @@ static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, ui { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } void @@ -560,7 +612,7 @@ Hacl_Hash_Blake2b_update_last( FStar_UInt128_uint128 totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len)); update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } static void @@ -624,7 +676,7 @@ void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash) KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store64_le(second + i * 8U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } /** @@ -965,7 +1017,7 @@ Hacl_Hash_Blake2b_hash_with_key( Hacl_Hash_Blake2b_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2b_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 16U, uint64_t); - Lib_Memzero0_memzero(b, 16U, uint64_t); + Lib_Memzero0_memzero(b1, 16U, uint64_t, void *); + Lib_Memzero0_memzero(b, 16U, uint64_t, void *); } diff --git a/src/msvc/Hacl_Hash_Blake2b_Simd256.c b/src/msvc/Hacl_Hash_Blake2b_Simd256.c index 1a5e8cf2..7aea4d42 100644 --- a/src/msvc/Hacl_Hash_Blake2b_Simd256.c +++ b/src/msvc/Hacl_Hash_Blake2b_Simd256.c @@ -26,6 +26,7 @@ #include "internal/Hacl_Hash_Blake2b_Simd256.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" static inline void @@ -214,6 +215,7 @@ update_block( void Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t kk, uint32_t nn) { + uint64_t tmp[8U] = { 0U }; Lib_IntVector_Intrinsics_vec256 *r0 = hash; Lib_IntVector_Intrinsics_vec256 *r1 = hash + 1U; Lib_IntVector_Intrinsics_vec256 *r2 = hash + 2U; @@ -228,10 +230,61 @@ Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t k uint64_t iv7 = Hacl_Hash_Blake2s_ivTable_B[7U]; r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3); r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7); - uint64_t kk_shift_8 = (uint64_t)kk << 8U; - uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn)); - r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1, iv2, iv3); - r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7); + uint8_t salt[16U] = { 0U }; + uint8_t personal[16U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 8U; + uint64_t u = load64_le(bj); + uint64_t r = u; + uint64_t x = r; + os[i] = x;); + tmp[0U] = + (uint64_t)nn + ^ + ((uint64_t)kk + << 8U + ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U))); + tmp[1U] = p.node_offset; + tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U; + tmp[3U] = 0ULL; + uint64_t tmp0 = tmp[0U]; + uint64_t tmp1 = tmp[1U]; + uint64_t tmp2 = tmp[2U]; + uint64_t tmp3 = tmp[3U]; + uint64_t tmp4 = tmp[4U]; + uint64_t tmp5 = tmp[5U]; + uint64_t tmp6 = tmp[6U]; + uint64_t tmp7 = tmp[7U]; + uint64_t iv0_ = iv0 ^ tmp0; + uint64_t iv1_ = iv1 ^ tmp1; + uint64_t iv2_ = iv2 ^ tmp2; + uint64_t iv3_ = iv3 ^ tmp3; + uint64_t iv4_ = iv4 ^ tmp4; + uint64_t iv5_ = iv5 ^ tmp5; + uint64_t iv6_ = iv6 ^ tmp6; + uint64_t iv7_ = iv7 ^ tmp7; + r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_); + r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_); } static void @@ -254,7 +307,7 @@ update_key( { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } void @@ -295,7 +348,7 @@ Hacl_Hash_Blake2b_Simd256_update_last( FStar_UInt128_uint128 totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len)); update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 128U, uint8_t); + Lib_Memzero0_memzero(b, 128U, uint8_t, void *); } static inline void @@ -371,7 +424,7 @@ Hacl_Hash_Blake2b_Simd256_finish( Lib_IntVector_Intrinsics_vec256_store64_le(second, row1[0U]); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } void @@ -822,7 +875,7 @@ Hacl_Hash_Blake2b_Simd256_hash_with_key( Hacl_Hash_Blake2b_Simd256_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2b_Simd256_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256); - Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256); + Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256, void *); + Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256, void *); } diff --git a/src/msvc/Hacl_Hash_Blake2s.c b/src/msvc/Hacl_Hash_Blake2s.c index 652c3f33..37fabb67 100644 --- a/src/msvc/Hacl_Hash_Blake2s.c +++ b/src/msvc/Hacl_Hash_Blake2s.c @@ -26,6 +26,7 @@ #include "internal/Hacl_Hash_Blake2s.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" static inline void @@ -474,6 +475,7 @@ update_block(uint32_t *wv, uint32_t *hash, bool flag, uint64_t totlen, uint8_t * void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn) { + uint32_t tmp[8U] = { 0U }; uint32_t *r0 = hash; uint32_t *r1 = hash + 4U; uint32_t *r2 = hash + 8U; @@ -494,16 +496,64 @@ void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn) r3[1U] = iv5; r3[2U] = iv6; r3[3U] = iv7; - uint32_t kk_shift_8 = kk << 8U; - uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn)); + uint8_t salt[8U] = { 0U }; + uint8_t personal[8U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U)); + tmp[1U] = p.leaf_length; + tmp[2U] = (uint32_t)p.node_offset; + tmp[3U] = + (uint32_t)(p.node_offset >> 32U) + ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U); + uint32_t tmp0 = tmp[0U]; + uint32_t tmp1 = tmp[1U]; + uint32_t tmp2 = tmp[2U]; + uint32_t tmp3 = tmp[3U]; + uint32_t tmp4 = tmp[4U]; + uint32_t tmp5 = tmp[5U]; + uint32_t tmp6 = tmp[6U]; + uint32_t tmp7 = tmp[7U]; + uint32_t iv0_ = iv0 ^ tmp0; + uint32_t iv1_ = iv1 ^ tmp1; + uint32_t iv2_ = iv2 ^ tmp2; + uint32_t iv3_ = iv3 ^ tmp3; + uint32_t iv4_ = iv4 ^ tmp4; + uint32_t iv5_ = iv5 ^ tmp5; + uint32_t iv6_ = iv6 ^ tmp6; + uint32_t iv7_ = iv7 ^ tmp7; r0[0U] = iv0_; - r0[1U] = iv1; - r0[2U] = iv2; - r0[3U] = iv3; - r1[0U] = iv4; - r1[1U] = iv5; - r1[2U] = iv6; - r1[3U] = iv7; + r0[1U] = iv1_; + r0[2U] = iv2_; + r0[3U] = iv3_; + r1[0U] = iv4_; + r1[1U] = iv5_; + r1[2U] = iv6_; + r1[3U] = iv7_; } static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, uint32_t ll) @@ -519,7 +569,7 @@ static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, ui { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } void @@ -556,7 +606,7 @@ Hacl_Hash_Blake2s_update_last( memcpy(b, last, rem * sizeof (uint8_t)); uint64_t totlen = prev + (uint64_t)len; update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } static void @@ -614,7 +664,7 @@ void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash) KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store32_le(second + i * 4U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 32U, uint8_t); + Lib_Memzero0_memzero(b, 32U, uint8_t, void *); } /** @@ -925,7 +975,7 @@ Hacl_Hash_Blake2s_hash_with_key( Hacl_Hash_Blake2s_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2s_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 16U, uint32_t); - Lib_Memzero0_memzero(b, 16U, uint32_t); + Lib_Memzero0_memzero(b1, 16U, uint32_t, void *); + Lib_Memzero0_memzero(b, 16U, uint32_t, void *); } diff --git a/src/msvc/Hacl_Hash_Blake2s_Simd128.c b/src/msvc/Hacl_Hash_Blake2s_Simd128.c index 73f0cccb..ed86be43 100644 --- a/src/msvc/Hacl_Hash_Blake2s_Simd128.c +++ b/src/msvc/Hacl_Hash_Blake2s_Simd128.c @@ -26,6 +26,7 @@ #include "internal/Hacl_Hash_Blake2s_Simd128.h" #include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" static inline void @@ -214,6 +215,7 @@ update_block( void Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t kk, uint32_t nn) { + uint32_t tmp[8U] = { 0U }; Lib_IntVector_Intrinsics_vec128 *r0 = hash; Lib_IntVector_Intrinsics_vec128 *r1 = hash + 1U; Lib_IntVector_Intrinsics_vec128 *r2 = hash + 2U; @@ -228,10 +230,58 @@ Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t k uint32_t iv7 = Hacl_Hash_Blake2s_ivTable_S[7U]; r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3); r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7); - uint32_t kk_shift_8 = kk << 8U; - uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn)); - r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1, iv2, iv3); - r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7); + uint8_t salt[8U] = { 0U }; + uint8_t personal[8U] = { 0U }; + Hacl_Hash_Blake2s_blake2_params + p = + { + .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U, + .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal + }; + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 4U; + uint8_t *bj = p.salt + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + KRML_MAYBE_FOR2(i, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 6U; + uint8_t *bj = p.personal + i * 4U; + uint32_t u = load32_le(bj); + uint32_t r = u; + uint32_t x = r; + os[i] = x;); + tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U)); + tmp[1U] = p.leaf_length; + tmp[2U] = (uint32_t)p.node_offset; + tmp[3U] = + (uint32_t)(p.node_offset >> 32U) + ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U); + uint32_t tmp0 = tmp[0U]; + uint32_t tmp1 = tmp[1U]; + uint32_t tmp2 = tmp[2U]; + uint32_t tmp3 = tmp[3U]; + uint32_t tmp4 = tmp[4U]; + uint32_t tmp5 = tmp[5U]; + uint32_t tmp6 = tmp[6U]; + uint32_t tmp7 = tmp[7U]; + uint32_t iv0_ = iv0 ^ tmp0; + uint32_t iv1_ = iv1 ^ tmp1; + uint32_t iv2_ = iv2 ^ tmp2; + uint32_t iv3_ = iv3 ^ tmp3; + uint32_t iv4_ = iv4 ^ tmp4; + uint32_t iv5_ = iv5 ^ tmp5; + uint32_t iv6_ = iv6 ^ tmp6; + uint32_t iv7_ = iv7 ^ tmp7; + r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_); + r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_); } static void @@ -254,7 +304,7 @@ update_key( { update_block(wv, hash, false, lb, b); } - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } void @@ -291,7 +341,7 @@ Hacl_Hash_Blake2s_Simd128_update_last( memcpy(b, last, rem * sizeof (uint8_t)); uint64_t totlen = prev + (uint64_t)len; update_block(wv, hash, true, totlen, b); - Lib_Memzero0_memzero(b, 64U, uint8_t); + Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } static inline void @@ -367,7 +417,7 @@ Hacl_Hash_Blake2s_Simd128_finish( Lib_IntVector_Intrinsics_vec128_store32_le(second, row1[0U]); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, 32U, uint8_t); + Lib_Memzero0_memzero(b, 32U, uint8_t, void *); } void @@ -788,7 +838,7 @@ Hacl_Hash_Blake2s_Simd128_hash_with_key( Hacl_Hash_Blake2s_Simd128_init(b, key_len, output_len); update(b1, b, key_len, key, input_len, input); Hacl_Hash_Blake2s_Simd128_finish(output_len, output, b); - Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128); - Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128); + Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128, void *); + Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128, void *); } diff --git a/src/msvc/Hacl_K256_ECDSA.c b/src/msvc/Hacl_K256_ECDSA.c index f9bf31ed..0aaab085 100644 --- a/src/msvc/Hacl_K256_ECDSA.c +++ b/src/msvc/Hacl_K256_ECDSA.c @@ -571,10 +571,6 @@ static inline bool is_qelem_le_q_halved_vartime(uint64_t *f) { return true; } - if (a2 > 0xffffffffffffffffULL) - { - return false; - } if (a1 < 0x5d576e7357a4501dULL) { return true; diff --git a/src/msvc/Lib_RandomBuffer_System.c b/src/msvc/Lib_RandomBuffer_System.c index 0d7924b4..de6ef337 100644 --- a/src/msvc/Lib_RandomBuffer_System.c +++ b/src/msvc/Lib_RandomBuffer_System.c @@ -31,6 +31,7 @@ bool read_random_bytes(uint32_t len, uint8_t *buf) { #include #include #include +#include #include bool read_random_bytes(uint32_t len, uint8_t *buf) { diff --git a/src/wasm/EverCrypt_Hash.wasm b/src/wasm/EverCrypt_Hash.wasm index 101c3f6834aed5d76bde19f1242639e8d080fc39..a5f05d9df8aef198166f523bcfafc86a034516b0 100644 GIT binary patch delta 2618 zcma);e{5UT702Iw_Ir-~p6!<(P8vH-?u*mdFF37#H*FIqPFg7W<(7^~V`Gs4mn2O? zmV_uNgqVsJq|rckXay8Twys;HQgC?{Lo0s-A@K(jktRT5MXa##2mio27@9Ojvh&^z zS*lL7|J?gM_uO;d@#md)ub+9?^8UYhH0EYg&xU^vAt5YjjfcyvNc7@At}TwDy%=ujpUsZgSl8THE{pfJ-Nv|d?Yl$f>2H> z;eyaas^GGaBpYz7hb>|`sfHdgO1v;D#)uD!IM%@5L=E=a+~BkM;g_}m{Me?zpKx9f zByl7+G09PQ!4@Mbj`i?Qn?mYAD2b2&q)MWs0S0m02oF1`{b%>*^9S=0t`V!-Eaax9 zxgfO3Rp7E$$RYdAsr-1?_{`X32s(rY5#2FPGyV73J){W^+ndNuP_&0h7(TLxNHdNN zmSi*rbB;zK7E5rO@hJ@g{#Gu6Dnz1&E#eL?W4U6OB<;9RV`qT5j-avb%8lGRaNoXxiAjXc^%)yr(P`uR>kO}L-*`UHWlb#(VwZ5Y zf$aL1Yp>(-+lLCA|AU`nE4iT5?Il*Y(pRnL-EUdN440vb8}c5_83_>U9F3SO3M_b{ zjwp?ywa6)@P*$b6VgVjE#Mn|9d|XFiq^h~BTrHs`%^auNGk^c~)vsrj3OHL;oAh{@ zDNr6$j8H;3rBb@uqP7gD3aUs2DyBG2dK{Lkda;29sHRVDIBX#;kn692%hXdErxr{z zswQZh@-(5eK%%A%yX>=o1}AGOu*-@y+p)_?un8*trKm!F!yXE1aMWLhYQg^ptIwO^ zpfpt&4w?!1J~L!LEF^u7kwkycP#H%@RMB5yuZ<(Wk-d)J5u6YY7mF z&(`#?dXXop{#oEt9^126qeu2l2u5N>M#;W!NxXin}eqP%rl1A7NN#NLLjxDVkoQ=q6KY6YK zR$4v!Cy_3m|3=Uo;}7xVA5hdb>Tf4kZ2Zv@{7qHx=d=P}wk`38ZL8)!!;@*>x_-mg ziE4Pgz0KJ44SLvKy|07kJ(~Iyp-&OxO&=$#ueu5D>8$6^I`qdne?!WG>NK4;{4=ZW z5Tti_`Qvu|jvdo>vPFNl?>U0gSXPzDR{a-uY`5UFbZ6FvQ*FN6u!aT;R?-Un<6-FD zKMKX!1kMNG$=@}Y_S{UPZ>yI&sPo*c>Zg^|Pkq#>Z1bWd%63?sIRr0_Vcfwa&Ssqc z(%1`xwCeriUyu$1W|CW5~_dIJcQd4@ol zU(uDv*ASS?h(MXY4uaiJtRWDOjp`k60|}Nl zon$GOPMQctpT7=*<-!p_2Dx%9^d(uQ(-9lc2t+o zu7~!2(iL88x6Jj*l0-R7-y=Ji*d^PUxJ52u;%3>##7RcrG+?;CgMoBh)IF{$RKbge;CXKxrg-0QN>aGmPT@^* z)rORWFpL{)HCa%#Q@fGf@!eUZN_cEYc!G&g4z-;j1;}%dX)Dt0Wyc WhO`M6;3WL3;P`!~{*%|*O8yJ9{>>u* delta 3225 zcmbtWYitzP8NGMB@16B7#s;(Yns5Bv0b};zUBB%en}^>IUV)IX*)+>@y*8|&5Wsej zortDMYCa$}Y5*xMMXB64nKY@2(p0J{s-$fcRjvAm^bu96+8?Bes#cYN-n(}_qEC?e zW9OdloVjQ2oO|`n{^IY_{4;rOlE{owLI}MyGd)eV%(;i=hTL;Q<~L^Ep_cc~GplDp zzLmKDpXr^%W5>8TLYLtMb9hC8X-6WJbY=D@LXl|v==f8Ki6mK$9hUNQmgTe%3oUDC z5i28f1t;-k#;(L~S%S0}Z&^Zg6?&{8>cuXrN=tCmx|WvWJ!?7MuzE0Mb)(Bxc+TQP zwECrRBfe`5;x?NH?=mH0E2j!xv;}E7{+L}W@V5@IA3mB)KAjAZO18T7=ESk%qzYe= zS7O>;C|BDz9!nnSI&xxs!jD(Yl@=z4NKID%&|XCS_rs-nkHOV?nV!%x?;Yo$37 z43S#qUTF@6>d88RB2iMuke{y4*8H9TzH9R0fK#PG{Gv0AA!h*&n(g=_r;5j%1?S{) zT8|a-8@@=ip|PpCrM0cSBc^qBZP>VJb9YZ~U;n`1(C`TUSss*LT8^4)9c{reSB2CH zIPNOJ*IgD&yL|Rs$n7+2*t0``G=Z2>Dj2e>GRFdygcOWFU(z``MWw z!9~9(H?`)l+nm{?}jLq@;h@{cF>d5`guZNuw#vlsc#c zSz%i$LadONim-P3&f9-E?QtvhQ12&1i5Nr_qJCmh8VsTl8vVqkG#NxQH2aCHv=~Gy zwEBrhY15{bT-%}DPYRU|T};!6W}8qpKt!9Kp0U9O4KkTbtFjRSu#wLR2)}^v3kbiU@CypR zpzsUk{P1w0TCk~tnx*h}OoU?PWzaT3+Jw!?Onz?8DXU><=-RN_~5 z8pJNxrILX1s6p(8-70BR9)ms@Y+zCJ!Egi1tq-;|5Dy!+HIQQHhaFt&hn-yOhex^A z505cTBMX{s;aTNz80^f3`*@f31F|qXJFD!09@xX@^$5=%;n^cRdxdAO@az?yy*W?( zU7_lVS4b@0xbg&xH;gZ~uEh6zE^I1VSFlX6fo&a&%bt6W0z6(+7Fq5Ur5Pl)h7?dB zo}e}>`J|Dyw|boN<8gt zVSVnWm22=5?=psHm5OC01q=mCxH4MuJ=OvJr7`+*9I1}tmC~E67w+@Lq#sJT#UEmA zQ9NfgYmM=;2I|9?*|m&4NY(#Vc0;18+0#`0mck&gN2<5Sfj0a02_+0f3)I-#UlJvYy|12;m(Pxmh7xN9!FNW_~ zrB@v6ooev=EkBbk*cm*{8CP4=k}%e`g9|qqlhuoLZ#$KWYLxR7&Qrd17iezp{1}Lp zOE+YFTkPw!ph`Io$GLtYCs(7R(<^<$saJO%x6_DzrSEH0igEu2<-umXHg0xnOZmqF@j z!cR|~!Kc${9Nr&c<0xK9ROlztS82{8D;=s|lJG=&3|~K0{Xol)Gs5!YjIg|w;g3O@7P744kGL`mp#dK z{3Pq|zuGS0vsY@R+xdF*8n@Ehuiu~bf0)z%T1Vbfy|U8@gn9JH4gogFb^$iZHUT!s zRsp(XivZoSS%A&5Nq|l{PXJAp1c=F0fDXL9FeJU;(PQ7c2}qz4*;zw4g?Dfs2QhZ*-5VdP!H<43xEe-Y40&o_Ok6*Z&uSy&L~r z=cZLDcCd3FhY|i=-8&WJ)4;F^Wo_=Sc`!8FjsrXz0oU_z1gzun2)K?1Bw#I%NWir` zBmoC`Oacz^peS_kKEH-%C1_P9POz~LmPN6G1+4so^`&X{Kaa3a;)}};R+^m7i^yuq h2q*ia`OCLD^A4mB;74zd0Jn_9GS7J_P zdS1Ml2?NW-a|(>ClZ6;H8QCV=Fv>BqPp)Is-h7(Th!M#A$D|7+b(k$BIHVjIG#D5h v4=^|~=7120mnFb5xt4jEI80IiLoP;EQ9waJ0Hy##_hyy}j4Yd7SdEwfMYJnt delta 200 zcmeyy_l<9YyewlqV|@Z+9aBA!1T*0TbAA0pn~upkjGT;&lg$_v7?~!XlV>qDVql&e z&Zx=AGP#jaj*)fZIVDE6$qN{@8QCX(RNQ=;(TI_eb@D$ZT_CB$Y$?Gm<;bAHz~Fd* u!I3csgh0G30mjL-%*(`Kk^&fVF|vvR3IYN!1sJ+FvrJ%Q-0Z??!~_7Kr!6Z0 diff --git a/src/wasm/Hacl_Ed25519_PrecompTable.wasm b/src/wasm/Hacl_Ed25519_PrecompTable.wasm index 46a7380db06358dcdef5459264c6b9f1dc726630..c94538f0c5740cc5e275c8a82bc368902b64046d 100644 GIT binary patch delta 103 zcmX@yz<9WUaf19rOQDIXA`|_&Ci=&5C8d_+=cF1NF)&UnlxHzCV_=#*nNg9Ed19gD z#I>A^EEBgYFtSekt*OAq9iCX68(dmYkY7|HfW(e3DM~D0V4s}MsJ(d$W4|2$i_0N6 delta 83 zcmX@yz<9WUaf19rZ7F8v`ud5E5)=JdCq{;FCFW$N=f#_uFfdM*XH;Nhnph~$Vr;~~ mJlTO!laXa|7NZ;^D@e@HjDc-(C!;na`@~y{o3}9b+W`R5?G`8i diff --git a/src/wasm/Hacl_HMAC.wasm b/src/wasm/Hacl_HMAC.wasm index c2e51b851c0e3a3f21be3160b08d2c2ff85f9351..4837783c3caf2566c5fc53b594b01adb3cef5172 100644 GIT binary patch delta 4288 zcmZ`+-BVT96+c_9kw|BX6N8ni`7J>N1V2!e4+Rb%0?L=7sK_^na=9Xk#zfIe5{)s@ zC^=DMqPC5i_)upuuUTgh+d+ojU zT8BUV+sysbEcb?IP8-kj%>DW0&oeTT$@!nw+t=Sa%Haynm8XkU;5pf)+29Nk67zhSKc~mmi+mzul}*Dr1|atKA4;HmMpnC z^=jRkCFa#HyNZ{r@jV~et8=kl@{l9>i22^$Skljy4cHKL_7?0YK!NY=^gL|v&7^F| zsN=xfAFK1dLQWP?iY4MGppZ5SWckXP0@>)l_OKCo^_~uLvU78NZz+dTh!_f|q)1=W zQj8)ZqL|EQV@V3+*%SbI@0Fkgn-sQ$mYYzRnB3`cfl`VR*^JG>*{uBDE!cu0wb_DV zr`?JzvJKm^qzq*YFEinrM4aoB?Th4??7((nN;xuQCo)h@J2jPE48H;uHvCFdy6`J> zSrrVwA`*TjB@Mqa4Br`P`0rFol}25q;UmX4*}u*W=DIKDVmqf3*n>P2zQj&!r-FPn zsIh#tsC9fb%2z|anh0MlCFQFP`J9pRt*@0j>_8pz2>%l0FJ~$3vRj^&>qC6_f%FyZ zs7Jl;RdKs~#rKKtNAT-)n)vmlUc^Z8d+VhE4bq4PKRdNgO~{kIB#h|?uL5-=KmIu+9O4UQ?mcuw~Q?&;@=u(>=9B`?61U+&TN3-M@ zj*&E-s=bTkm>fqhF{KY3(vJ@Gh5IQ3Or1dt+SD1skV~CGUDhBsVvvhXox>0%O`V}| z@12nbzj{c9HC2ags;;rAO4t#MSlCgFI@l3~9U<&U1a_2?!j6Wp&PZX`j>;H%ZL*Is z**jmNAH6QwPvC@w9>=(YKB3Sj2z?>~Jx)oX$3tjmq|ocedBu`3{y^qO$90Qu{ zkW)Bi6MX^`F40dZ_9lsbgGlaK^K26W*h-X5j1iuJ z80-{Ex2XL5vC?e%G4AF=8SA$O|n-h-)%-S@hxYw<7{U6r)GOA zTCvM2TAiYmRlS8rk!|}1A+awi&B}iDGi?^Pos~VrZFlbN(xIA_o#+g4JDs9ax>T{^ z0E>9&a=>bWzl;^H2yMHaZMPhU3mL97(f+L~gh*KPqqpC=%_Gci2ktFkMEq(2Ww_mdG)Bjzv6&D5X6| ztd#N`Q_nG7m_HzFEi%q;fs-2O|5yE!TJ_z>!1%)OjSf&ZK;P8YzyxCo3nBAG;#46% zC6o3&EeT9=%a8~Q5wR!bv=$;v@poDa(Uh8=Mm$xC&R|NWF>Nam3p)5s>+zLvmFOHx z{0wHYk{|$ z5?7n5M3*V)g}oe}fEoo7&&jwfvzo<4S8&C-+gB#8$W`tEW*Oa8=y!sx4oM`Htb&?3 zLPvel^39o$(3$DM#kjQ}1^;Tx4?4=;+8Vco;A0DxiI0tZVsL@X34CP8 zP3Z$%aOBqvt{J5d{?oj)!m(d7N`K9epTl&#*VWdp;CgBWp=sc+dN+36$fvr5)i(@o z7}D8Q+z3~3!^mf5SA(14FqJ`9x)jeKix%izmJf#U8W(bhE@eHER}#Mg_&S$tvi zxgVWnb>q}GI`xZ%E^r0k2J`K!*WEJmox%I~R1?CEKGXuoJO9YwQ7~OmSpC@GF`e~) zokun!9%)8!n9c~AsET*su?fq7H4VD@S4})N^2FeYk>BXwbfx<(Ddl(kldg5&6I7lm z{8JMtT6CnGE?ac6a;k7qVC8xmm{qGPpQ-n=s5f~ir@g-q<&-y-^nRwf+s;)!H+XL3 m2Ln%jG`bNl6!Aqg+#ij~VF9G&f)K`TWqF~9=1GuqKL3Ag=8u^G delta 5458 zcmbtXYj9Q76+Vkx@v2OFs}YbAyH*n74G-mIB4{utJOkzh0rC(oNeBeE31GrAj~l8% z6a>Q|R0S*4s#S;u;{#MQh+43%kIGE_VW<7s={V!B{%dFYt-a4Z_r@82b>`%pwf0); zTWjy^z4mu|zomEoNjEzU?XBcE4jt{k`K6mFL5X#v6NyAm|M}bcKOarh|JQQ5K9om` zLPZmnG&IFyrLEiIv66VhmgbqU`CHrCI~v+L+QpcbG_<$)ruJAYwz0V*wrOW|Lu0%- zw!#~@;l%%iP%>0Ix`sww|7K|D#;J>M`sVrGUT4&(p69&b8wb3@6WfOVRWW%~LUK6U z4Y?F|L-Ea$3niRXCP5jKRPx;K|NHj8yCZkVU3^#6aU>cHSW5yz-1QCiaO(Eb}(=+-y3x%N&!#eXo2J4 zGr7PC;WM?s3FC8jfis5lc)Hs1c&6I&c(&T|xBxcSal;)_$Wgbq_pvY+y4>F0UMlx- z4&SFSITkO+;^kPpT#J`$@p3I*uEFDMnZsjcE{9xaQ7GYMRqq<-4m(`Lb4nZ)#zrPg zaGe_9uGoXfq_Re7^3xWaWbWw}dRq&%Y-g0n1C>^fLju7HOB1y?{xIeFX1 zWZqFBl?q&`8F;Kqk)Ka+BT~gx26j0wx3ED}Yq_l8QUJ$! z1<&DmgZvPeTIg!7Hqa}1rG>6m=xRV$r$MiTrqC;WXzQfV*(+rgFXdG{2k?WuY_JPj znOT=xCb%rCd9_zrn>V|LYg}h8Ccj$oR|9`_8h(uq1HWdPljfxOH8oPpwNl5mZbWw~ zyriDz$iqk&Z0a?xBWnS<)(w>=7r9O~^*6u|8*Q^+{#utdd*^<7`@M*ZAug5{SFc(S zx5jA6xESIjrezh^$~s;r4LnyGG0P@^G^Nd_5gKhVnHvJppPO2wNkI~|F1w*fcmg)r zdd#UgeNG#o1P65^lrcINJ;E))f!V~HFeBL<3~b>odQjuRKr6TEL2U~Lw(?dzsM~ZP zVNUyY-mWM0k-(*$+x4J!1Oq#GhaS|O!N4xwr3ZC4Z{*Fofj4qo593B|)5Extx9LG` z;YZZg!X0XB;hk!0;oZSO-IL(W_N4AHCsp=xGw;=yW{cNs@tQ5(28*}B;%%^a8!XW&aOGLh?8< z20P<&fOx$;ffpYz#ps@Xl5oxs5+5Wzjzx!v4*^dz9)!;pn6Sklrn(4RpzEnTME<_^ zUA^;}x8He)B7NjzdK zBHp&y93XTX3_MBNZ&;2IA0zEHMFYeGfYyF<%w#*J*&wE}!9`8THbDN#^j$UErU8=U z#K%c~rSDYlc?QYlS*;-GKF@dNLYDM4v>h<4d0>exBsl#E!f`Scg-Jb}D_cFOcefM}lLZ_%k=UoC4ao zQ7(J`Xw59Ub{1?RZ&Z&Ys0SSANB%N;qOj%ss9obSdSvLkx|tbiOeCDnL{tfwh$=}Y zlBG-}A7?4aM6v`-Bp>}O$waaQOe7!OE6GH%1WY6!%__-6vII;d-{BM!$r3P;d?y+( zkt_id$#AAK(W{oIHmGXH!4@O{`PnhS)gD!d-I1C$MY~)VE zVR}i5ImE?n;_7Fcl(38A!X5qd}-;$^^;GR^>>%HT5X*V-a0Fy%_F z)G5yfBeJuq)UqnE-z!mU^6syKrYljUD}frUlU})Ac2j*CHD}bz!`|hoIk&IjHNZDH*VvqEWUX3e#W==g z#t^fH80g7bta8LG9UysKy4EEP8b^%=w~3pQxJ@>^N!F|7)@EGA7Pr|Nnmt|+&49PJ zbU^`?dHc-!f_Z8eF~3=!-=Y?28kFbix*|ANtJfQ9&6P&F_RpA4$@DEX``%Tf^(1~L+i zfpF|6?U;|J#y~#~U@QU(;`=4Cz&~(}YU2clu)o-{#E=l}ogfm)F~c6TdxAM6$8hmK zjo9ge>pD4R?tAT_xUErfAL+ju!s8IaDm(!pqQXHcOrX1gPCaFuARIAH5c-W11P?;c zRdLVvk?pIvvhlM+`zr2ptlEHqfMD}Luz4UL57J;QZ5jwR4TNHw2a?T$UWhw?*ul-; z1_EHEZGt-)3VPx*cpF{`75~F$N!z0L^z6|&&yw~$FaiYQ!aq*Q-gtsADkpJ^E1yi5 zD;sF)4fz=eN;+{h<0i*#{Q@}UDRWP!bIQ{{7zxR5h%tyX@}lz9-{QqDqA1%jUs6)} zGV#k4xe-ksEYT8~u=ibTT+u7UuaKTp2M#)qmkGNUVru)s1v>T_JoSvET$LnwqaKuk?fWrJL$!mo6z`w&T<=2RncA74DhWHF=A1pdceAdr<#^gPtc_F6q!UekKJ)6wy zyK3IhS&~6-#;n}AuM^`rZhPYEehsga{9cy@WyE<<>wt=tIqg?+j`*Cdo`1>$!{%$DCDp_@l)QbD$IAth zKM>>OyrFx;iZ78~D`?YDl!(#oIlvOgiTi+>JS`9c$Xk^Un9fzVTz4}y$t?kf}q1wR75 zFh3!_)aWnMqmc)CD*AI@Pe#Lt=r6U_GF15$@mC~&A$H_z?O$?T5wE9D_-j(#zt7+q TDE^IRbh)mG^qKczonPV^I-7|l5`dii8kMo~tl$#IMdjLehk z88sPMCZAx`W@MeXL7v6XjDc<921%~OoXqsRcrz0Q_Q@+5<#;$aJra|1;yrvFoy8^> zFo|v!VG?HMV^vgeJiy?{m;*!t%#%%7Gk94QB^(XlBCEh60*(rB5qUO{8V*MhxX2W? zE}%h<$Oh@KgA`dJ8MF{AVu)mr7zap=CXzwj963P${NPYzWS=a>d5Dp9@?B18M)u7= zIcu3DSfv~pG#D5ZwlYF22J^B6*f;m_{APs99!8g4$oGj6ZqNn+2PPorqmUTTR1V>H z2z`^#_3?>5L+BF}H)IlrIUpF#{z%DfAe92rqCi8{q&Fe7eU(Adri7-=R(=~J+)QYI z!~Mji2zK>fB?+LJV#>J)hxVg8bhgTSgzQ{&*+ps}LGFPVv{u6z#QCTRaw)skDun%| zXpTFfy$hjjjxJc+13i$oZ+fdhG7Akrob3i15Xu^joDl|!qZxSH7|AwOG|4%p5lm97 zil><&F?^C4O`gv}10??vD*qf^KEP@ZGtf=EcA(Hwv(o^@vA+X|li{!o#Nl@aaWtG2 zLB?ETf>?8f3C)^h*VQ0n_&vdjJ;92XLG4_EZfCOh0+3-#86k!(Mh|#dKShwu_5mQn zA_7)30~LRTD*lY2I0T|N46Hb88c65+2v8zri@XYqT}1-h4Tv||&UsNK1#Evg1N-SVtpPbC7&BMXzk(itl z@8Rp{EH=4-Np!OalQ1(MhoXYx0R~6L93T>4oovdQ!ONj2;b;ICSp^mma8!Vc$g_de za5##Xr`EQF2bSx=nkE&@*W{O7hQId+DDLkAO@|~a0YQc zYJyzKuC)qbe<_;dPH68!Xq%%8*7iUTr0tvDDv-=V0}yAs!3Kn~Mk8m0f#PTe-ZnY}z5Po;pPVC*az5a;3cI^0>xW;i>w@KRAN!rr95kf^!ap4A12oOY^ltU8^ zfEovci-Z8F+8YIn&u_yKU?2$VC34}rv`h#5O^ToKFC>@(jp@67!9_V2e7 zYGe1Np_DT2y>oD&{JV)K4C}KSTc-Z_fN{)mWATKSOr&l#e)kk;PFESsX=?#WBS)?NJ%! zVLLr3%?SQz4T1P>|L8dW%N|5I&s0@NkOOR;} zGCdNc!bpNtj)Dx7P76|@GlO|Bbf`ZMRa7-3`>Oaim>4U{91u&GO%*~_MkX>)@dhM` zDyXS4OwKg9bya$dmK`d#kYI7Hk-GM zc<@5wTO)qhIDaVM!TgU5zFsgx48CdZ7>UFAR@sbx(H)eR4c=V-r^I*KkS@qo3v*8` zm|n8L6%(J@V7XNcez@$^Qb-LBN>UC=k~2(>9F!CzIVh>%S>So3h>tR5kk&Zfs0qX< zi`dD2=eSUx-S|2*EHuMtxP<&Hg4#U7GB&={=?4#%(~E4GXUqJE%UmBFTjs?w t&z70hG!;;wNhm79pb|SNjZ{%&WNh~fnH+u|J)uabBujiMId% delta 1905 zcmZ`(O>Y}j6usjaH)GF?J)UvwvFpV5IUk-$(%>egNe!*?DujaAR6=6GCKzf+9A`me zQ~|1OBm!)Z8VwQ>3;qB~C9u?We*%>d+e$3iQ1KzUL2%!^c!*po*?PX`&Ky0TbI*Nz z=eLit&^kO&06_Wrx4H)Stc46SjTMw#o>oU;9>^zj5;F9|Hjf0c^4*EMa8>fR5P>(CNSpu<596fQMzA7rinr zie4Fg(JSK;^*Eex{p3@&jFmU94~L)VxXd5G$lGBr%p5*i- zrx$Tz0h45i$~1CR6NY?sM20xwqYA2OUkkrkZfe4Rt?#uq0HUaC?(g(7=pP$Us{t zYoH^PH83w!H?bgkCVHZ0Vp;S|VNN8{2XE7z@209|nl;liF&a~uAOU|_9 zOh=sI@tPOjTQUY!(jL_xlO54qBzu{>*-sU#J{z$#8% zrmNG-C*tl^#^|XUQP;Q^Q-h$cb&z`8qwF|cQJ!+w1b1!puBPkt8=}1bO7I2cbt%?cTj_ja?Lw3|Jku5x$mO5AVS)FE}&f(SZc==S((nSB% zcKJ~F@M``IpV5k<{S^m7Mn^|eO(Ar{ROz>socqrF=A1jTy{ymXAsP-C0I(-_ zCljbn^DSmhH;(LGPFQ1SLZht5h0NyiexX<@S27RM85@H-$Oz~2JrZ0O%%e{CMt21K zxNaMvGq}|sbwTPYM#IP=jcVQ?>i4%c!Jki+d$Tj_jG&Mnp#eqx-B@5H!k|%Zqy~M_ z%#|zNwP+Nzhuzy9lktZy(=2+++^z4XNe$zUGgfc{Aas-)y6E~&ZKjp0n2!9~84tZR zSOGv9^g`EMr5jkcR%b5sNV)wOy+!!Pr1$*tF)!o@p{Rp;#A4qDbQFYkm_ZveiLfqY zd|5+4h6b9LMa$3X>%13;8d?g@(PfR%ni(Y8eolYo>nx|6Vw*kJ^RnW-NY_RMxZW2n z%B0?c&udy1gRvP}#I%}J%cGZa3eA;!{xGzH78h%9+eg1+kM&zgF1)<9n3w= eul1u|XX$EtX}Nid{w=)`O!d3D$H|Z28T$pe!HD$$ delta 367 zcmbPi(PhfdkXW3{$iTqBIH9qjfkAX4ztzToV~py(4L}|bCl@ylFCV{vppdW#TRTXI zv7W*4BO5pSmL?#FQ*H7FCaKB%%xshEnb?`QRbgEA_?*Pz5(b{h>zS08_~k*u>_w@? zsU-{oKp|kdADFp@vMg=AXW(8ga76G2grrg<#T$2}ai!t&}-ofn+Bw2X6 zm?kk!p1>o*c@yM(CZ;;}$!mG6*c3UH85~zk?&lHRe1i826C?NJy#f~)xi|L-Ze|8@ zoJ8*fIZ9$@7#a6YelMQObeRQY$mAjk38gEnSpuvK3S5p1iX4iZ3LFZYW(*A6+&|ht g!NZ`;!2NOZ8i^T`&q=Of0r`1yz0}0bRZ=q<0iKCtHUIzs diff --git a/src/wasm/Hacl_Hash_Blake2s.wasm b/src/wasm/Hacl_Hash_Blake2s.wasm index 0dcaff92fc840a8a399b6410fb14041d83f27baf..755a6306aaca8d3f4d0bcf12347a7e5dd8e91a8f 100644 GIT binary patch delta 2087 zcmaJ>%WoTH5dZe!WWBq#*Y?_8Z~U0C>)L&|k35_J z1P&BbIDpiyK;nYnfO_fyMMdx@AaUWuF}?N32??OYfE@{b1!Jxc>Mj9%c}f*i!2$-&SY~=zEE^a<;v6@wkcyFw-jso zvkyrz%a_((8?9bi3tnGc8Liz|pAA+w-q_d_b|ZYGR;O>iHQL+|*>Fc~D!K44)vpyQ z&u83P57swD(W4Yk6>fM%^ZnAlAYZ?=zAnn)Z4KQ@`r6v&+G?=z?z*O!Up(f+ZvUvY zE8{1h(!Z*{e|{`QPY9fr1{z>E(|)8&LnB!1d%{64u~ebj6E6CRVFqS; z!oyl(s6)LcYS@4bI9yl;3Im~&a0kL5Q62~zvf!~V3qJd@P-9;f8swuEH=&ud_-a%q zwV5yAxgG<66ibBEP(+t*%st*rlqY;HY~Hx2FX4fR`>}CnBLzc+rRl$&B^*8K%uT`^agb&cdv2gQpN{eii`B=W6&eN z1u4f##gExa#YQO}u+;*SKn>b!2BeAF+W9Enj_&sD#){hFsd8+e3QJL(hB{HvJqYV- z-tM$T&G2k%i4GQpg^!x;0WC;0X_QQ9(5%LzM7ANALtd8rTKHL+!`*jf@`RY-H{iaQ zhG{OCq8}^@hnA#8STpY&oZdk@PdtnhBLwEfkAUsNRg0V1NUJuy zGk>sKfI_@A^1LPd|*YaAb8l_PCPgUZ9Cq$xKd?wRCw_qy1Fbp}z2_XZFD1}Ywb9{>OV delta 1821 zcmZvc&x<2P6vwO59jBA-B%P#_bb2zASIJD$$z+n<%xo6j%ha-~v+QB-g2bRBZYG0b z#)E<;!h$Cc+Tg*PsK-4>+{J%E*o#NOqbET`T)`g*zSouX3_%D~-h0)b?)rY~y}#dh zbe3VG=^1B?@y|Y(&spi?%&o6qyd7(PG{?v?tyDT=XLEU{P<-Y?O7R(!b8c=trQM0` zfNSNAv$rSb_gU%_t;*8@Xdcf7H?(pr=VH~3v3&5R=6O!>c=XC-cs!cEKD;>@ou2fk z!`I$AIbnt1OHDY%#H*w8(QtbI-4l%`fBT8vzW70_mlpq23!0tsfB}aXXpjQk#@Ezu z99tgfl0A<`)w zQlxe|N@O5IYTHpF3t3V-7bWtLC$*hbVkQbuAhnCD4BmqhsqIFIGL%W}HJ2-*0w$zM z9TRL))Px)$f`*(87lWUuc$Nj%};^$>Uc7ksY|D1^|q@=!Tu^a|bBjz!P zu0v#{a+0k(sjoX}tUGC~_p6QlItynAwshFA&U(YT7Y(cWwSs5KD~s~VqP(&wA6f*C zveuyv(lNr0G;qO=w6ImM`F5cw=X4u(fn)F86Aj2xXE9vDE0k5dtm5SqFQ<4p#mgz4 zjYE=#p9V48CYflxi0n!|x-e~uXnzRqgb@x^M#t*Xh3Vo$7c<%7ac-KJ>LI6h z!KuR@g%M~!j8>o?fqL|vM=fy$u86C^L?5^~K+3_T1NJfEr{Skujs7kVOBHcI5Z(%I HUw`x;ln#61 diff --git a/src/wasm/Hacl_Hash_Blake2s_Simd128.wasm b/src/wasm/Hacl_Hash_Blake2s_Simd128.wasm index 6d5cdb7834f987142bb56a6a2aec4f62a473dfd3..fd3c1b86281cdfbf43173dd093717f4f2d448d64 100644 GIT binary patch delta 746 zcmZvaKWG#|7{$NYKexLxvv+&{;(0+blYnPolmv-#Hkm*K5nD@-Ll3#lo)Pa-DCnLd z5mE%=NK{aXg=Gpou(LN>Sc$Dwx@cu7_{{}#1nlO`y#3Ah-t6kh_0u_Mb~^+B$g>Ci zK8$VT>b9Mx?-oCk+Ik;%!hkX!W^+-#P%M=*kIf!QLG5Ok_w6AHs`K`^*S^{A0X?o8 zmh?I+Nv{oDU$tshC~&J9bec)Bd<~)rqx{>gZmS1*b0jP%=%3akDI!K#rJ6D5%XYR@ z4z4$Q%|^FPDIz-_5Yv3LefusT?n*#NO#E}ca z8@UF|Ici6|DnJln30s81i9&tGJ5QLt<&7Q5y6V@T55Mm*S2)I`U|YCRR=@JrCSF=Y zoQpVHI{2}JgRs}8Y0OOZ1;370DG|}C{t;Btkx61QNih*s{>6ht3SvQHlT!H!He=K@ zKpiWfio}v0x`-2(For#NbKsk*w$DO@VHvtOqPeOZpuwPLcr5TxRrcBZADbIC{|{RY z*8DFP;ra^OBz&;P?${`9+ksv`J@*M(~~>yunaS!k57janKIbkDz-sj p3fQiGT6i8UB+aGPY_~Bpd+wC^5%orSMSm=g>xJUxpi_E5{sJ0zkAnaJ delta 398 zcmXw#&npE{6vxlKcjnEHJ7eaV8H#Wp@it_qP-^}I|G{g@(8Jrjc_|9R0x7~RVIdo3 zBQ&zJRZ=!ASjgH+Z=s}=dtcd|&$sXScFuQuaIN2gD5)R-KszgG3c;>3ay5R3id(55 z%P^^BH#u&;+4FPjQbNlR)^k+5UKL>U@k`vs9g^eASi`jUAGOkKl+?iD7q}ZcT~gMn zaT3?S6;iv{&`@4Z#zc847S86*hG()G$KVwkF>|EJ_l=3D7L}6nLQIf(bS!V;2jnDs zQv%}BHU_iZq3A&Q#atGx}!N9-4MlU}^{j zQc%RQG6XjG}ZBbyny9bYounC$%J>}090=9`1Qu4kIe{lk2-^N+$T#_QX+CNZ)z wO;^rfG~fO&g;AD~@%VO`G{(P-5TWP{MrKCF2ixN_K|*QSKvnay8Q%#50Q~YNC;$Ke delta 141 zcmccmkG1DN>jG}Z-|eHcr2KlNi~VIHaL6)4!!NT5i9S!YIeccxn6ZRK~xIXmWZPj4X_dueTd#g5+dj P`t-7a`qHu)-wOi(bqX{3 diff --git a/src/wasm/Hacl_SHA2_Vec128.wasm b/src/wasm/Hacl_SHA2_Vec128.wasm index cef1c90da828ebb4ad5cf85f71efe317b3c1a35b..549c8a5f1523879d3471e328a6b7732e0453a3f6 100644 GIT binary patch delta 327 zcmdn4vt4I`loE4&eLZ7+0wb8HW2%QS5rPxrR3|2Oi3x`%7Uu?+78K+cmBicfW(e3DM~Due4BA0 zBgbS1?oW*DlM9&VGO|v-$Rh@1zu-v_XO(hf&|qM2Fk$r39@ Kj?Gtvlb8T7_*s4c delta 274 zcmdn4vt4I`6fa{vV|@a1eLaX`oG2?fF-dV^V%NkI!Yqbn3``U6D>5=q+#|`An3I{F z7jI_5z%rSUQGtN_Gi41Id3Na&tYWFe8u?CJYjqC2Ynz qg)vKjeXeZ@wy=!~_6exkRb} diff --git a/src/wasm/INFO.txt b/src/wasm/INFO.txt index d2f1192f..197a9c67 100644 --- a/src/wasm/INFO.txt +++ b/src/wasm/INFO.txt @@ -1,4 +1,4 @@ This code was generated with the following toolchain. -F* version: 6e23042e74555544267731295b7d382c86edc574 -Karamel version: a7be2a7c43eca637ceb57fe8f3ffd16fc6627ebd +F* version: 7c8968bb0e417da75144912dcffd714364525eb2 +Karamel version: d9186a778bd8a730cc8ddcd84eac542fa7226a59 Vale version: 0.3.19 diff --git a/src/wasm/layouts.json b/src/wasm/layouts.json index 81273a66..6d56245a 100644 --- a/src/wasm/layouts.json +++ b/src/wasm/layouts.json @@ -1 +1 @@ -{"Spec_Hash_Definitions_hash_alg":["LEnum"],"Prims_string":["LBuiltin",["I32"],["A32"]],"Prims_int":["LBuiltin",["I32"],["A32"]],"K___uint32_t_uint32_t":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Int",["A32"]]]]]}],"__bool_bool_bool_bool":["LFlat",{"size":4,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]],["thd",[2,["Int",["A8"]]]],["f3",[3,["Int",["A8"]]]]]}],"__bool_bool":["LFlat",{"size":2,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]]]}],"Hacl_Streaming_Types_error_code":["LEnum"],"Hacl_MAC_Poly1305_state_t":["LFlat",{"size":20,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]],["p_key",[16,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Streaming_MD_state_64":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Streaming_MD_state_32":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A32"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Hash_SHA3_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"hash_buf2":["LFlat",{"size":16,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["snd",[8,["Layout","Hacl_Hash_SHA3_hash_buf"]]]]}],"Hacl_Hash_SHA3_hash_buf":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2s_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A32"]]]]],["snd",[4,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Hash_Blake2s_Simd128_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_Simd128_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_Simd128_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_Blake2b_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A64"]]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2b_Simd256_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_Simd256_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_Simd256_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_SHA2_uint8_8p":["LFlat",{"size":56,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_7p"]]]]}],"Hacl_Hash_SHA2_uint8_7p":["LFlat",{"size":48,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_6p"]]]]}],"Hacl_Hash_SHA2_uint8_6p":["LFlat",{"size":40,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_5p"]]]]}],"Hacl_Hash_SHA2_uint8_5p":["LFlat",{"size":32,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_4p":["LFlat",{"size":24,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_3p"]]]]}],"Hacl_Hash_SHA2_uint8_3p":["LFlat",{"size":16,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_2p"]]]]}],"Hacl_Hash_SHA2_uint8_2x8p":["LFlat",{"size":112,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_8p"]]],["snd",[56,["Layout","Hacl_Hash_SHA2_uint8_8p"]]]]}],"Hacl_Hash_SHA2_uint8_2x4p":["LFlat",{"size":48,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_4p"]]],["snd",[24,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_2p":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[4,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Impl_HPKE_context_s":["LFlat",{"size":16,"fields":[["ctx_key",[0,["Pointer",["Int",["A8"]]]]],["ctx_nonce",[4,["Pointer",["Int",["A8"]]]]],["ctx_seq",[8,["Pointer",["Int",["A64"]]]]],["ctx_exporter",[12,["Pointer",["Int",["A8"]]]]]]}],"Hacl_HMAC_DRBG_state":["LFlat",{"size":12,"fields":[["k",[0,["Pointer",["Int",["A8"]]]]],["v",[4,["Pointer",["Int",["A8"]]]]],["reseed_counter",[8,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64":["LFlat",{"size":20,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A64"]]]]],["mu",[8,["Int",["A64"]]]],["r2",[16,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32":["LFlat",{"size":16,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A32"]]]]],["mu",[8,["Int",["A32"]]]],["r2",[12,["Pointer",["Int",["A32"]]]]]]}],"FStar_UInt128_uint128":["LFlat",{"size":16,"fields":[["low",[0,["Int",["A64"]]]],["high",[8,["Int",["A64"]]]]]}],"EverCrypt_Hash_Incremental_state_t":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Layout","EverCrypt_Hash_state_s"]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"state_s_tags":["LEnum"],"EverCrypt_Hash_state_s":["LFlat",{"size":12,"fields":[["tag",[0,["Int",["A32"]]]],["val",[8,["Union",[["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A32"]]],["Pointer",["Unknown"]],["Pointer",["Int",["A64"]]],["Pointer",["Unknown"]]]]]]]}],"EverCrypt_Error_error_code":["LEnum"],"C_String_t_":["LBuiltin",["I32"],["A32"]],"C_String_t":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t_":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t":["LBuiltin",["I32"],["A32"]],"exit_code":["LBuiltin",["I32"],["A32"]],"clock_t":["LBuiltin",["I32"],["A32"]]} \ No newline at end of file +{"Spec_Hash_Definitions_hash_alg":["LEnum"],"Prims_string":["LBuiltin",["I32"],["A32"]],"Prims_int":["LBuiltin",["I32"],["A32"]],"K___uint32_t_uint32_t":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Int",["A32"]]]]]}],"__bool_bool_bool_bool":["LFlat",{"size":4,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]],["thd",[2,["Int",["A8"]]]],["f3",[3,["Int",["A8"]]]]]}],"__bool_bool":["LFlat",{"size":2,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]]]}],"Hacl_Streaming_Types_error_code":["LEnum"],"Hacl_MAC_Poly1305_state_t":["LFlat",{"size":20,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]],["p_key",[16,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Streaming_MD_state_64":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Streaming_MD_state_32":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A32"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Hash_SHA3_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"hash_buf2":["LFlat",{"size":16,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["snd",[8,["Layout","Hacl_Hash_SHA3_hash_buf"]]]]}],"Hacl_Hash_SHA3_hash_buf":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2s_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A32"]]]]],["snd",[4,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Hash_Blake2s_Simd128_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_Simd128_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_Simd128_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_Blake2b_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A64"]]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2b_Simd256_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_Simd256_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_Simd256_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_SHA2_uint8_8p":["LFlat",{"size":56,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_7p"]]]]}],"Hacl_Hash_SHA2_uint8_7p":["LFlat",{"size":48,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_6p"]]]]}],"Hacl_Hash_SHA2_uint8_6p":["LFlat",{"size":40,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_5p"]]]]}],"Hacl_Hash_SHA2_uint8_5p":["LFlat",{"size":32,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_4p":["LFlat",{"size":24,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_3p"]]]]}],"Hacl_Hash_SHA2_uint8_3p":["LFlat",{"size":16,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_2p"]]]]}],"Hacl_Hash_SHA2_uint8_2x8p":["LFlat",{"size":112,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_8p"]]],["snd",[56,["Layout","Hacl_Hash_SHA2_uint8_8p"]]]]}],"Hacl_Hash_SHA2_uint8_2x4p":["LFlat",{"size":48,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_4p"]]],["snd",[24,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_2p":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[4,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Impl_HPKE_context_s":["LFlat",{"size":16,"fields":[["ctx_key",[0,["Pointer",["Int",["A8"]]]]],["ctx_nonce",[4,["Pointer",["Int",["A8"]]]]],["ctx_seq",[8,["Pointer",["Int",["A64"]]]]],["ctx_exporter",[12,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Hash_Blake2s_blake2_params":["LFlat",{"size":28,"fields":[["digest_length",[0,["Int",["A8"]]]],["key_length",[1,["Int",["A8"]]]],["fanout",[2,["Int",["A8"]]]],["depth",[3,["Int",["A8"]]]],["leaf_length",[4,["Int",["A32"]]]],["node_offset",[8,["Int",["A64"]]]],["node_depth",[16,["Int",["A8"]]]],["inner_length",[17,["Int",["A8"]]]],["salt",[20,["Pointer",["Int",["A8"]]]]],["personal",[24,["Pointer",["Int",["A8"]]]]]]}],"Hacl_HMAC_DRBG_state":["LFlat",{"size":12,"fields":[["k",[0,["Pointer",["Int",["A8"]]]]],["v",[4,["Pointer",["Int",["A8"]]]]],["reseed_counter",[8,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64":["LFlat",{"size":20,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A64"]]]]],["mu",[8,["Int",["A64"]]]],["r2",[16,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32":["LFlat",{"size":16,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A32"]]]]],["mu",[8,["Int",["A32"]]]],["r2",[12,["Pointer",["Int",["A32"]]]]]]}],"FStar_UInt128_uint128":["LFlat",{"size":16,"fields":[["low",[0,["Int",["A64"]]]],["high",[8,["Int",["A64"]]]]]}],"EverCrypt_Hash_Incremental_state_t":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Layout","EverCrypt_Hash_state_s"]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"state_s_tags":["LEnum"],"EverCrypt_Hash_state_s":["LFlat",{"size":12,"fields":[["tag",[0,["Int",["A32"]]]],["val",[8,["Union",[["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A32"]]],["Pointer",["Unknown"]],["Pointer",["Int",["A64"]]],["Pointer",["Unknown"]]]]]]]}],"EverCrypt_Error_error_code":["LEnum"],"C_String_t_":["LBuiltin",["I32"],["A32"]],"C_String_t":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t_":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t":["LBuiltin",["I32"],["A32"]],"exit_code":["LBuiltin",["I32"],["A32"]],"clock_t":["LBuiltin",["I32"],["A32"]]} \ No newline at end of file