diff --git a/config/default_config.cmake b/config/default_config.cmake index 9b99d63b..ee7e66ab 100644 --- a/config/default_config.cmake +++ b/config/default_config.cmake @@ -120,18 +120,23 @@ set(INCLUDES ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Krmllib.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Krmllib.h ${PROJECT_SOURCE_DIR}/include/Hacl_HMAC_DRBG.h - ${PROJECT_SOURCE_DIR}/include/Hacl_Spec.h + ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Types.h ${PROJECT_SOURCE_DIR}/include/Hacl_HMAC.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_SHA2.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2.h ${PROJECT_SOURCE_DIR}/include/Lib_Memzero0.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Ed25519.h - ${PROJECT_SOURCE_DIR}/include/internal/Hacl_SHA2_Generic.h - ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Types.h + ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Hash_SHA2.h + ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA2.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Ed25519_PrecompTable.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Curve25519_51.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Bignum25519_51.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Curve25519_51.h + ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Bignum_Base.h + ${PROJECT_SOURCE_DIR}/include/lib_intrinsics.h + ${PROJECT_SOURCE_DIR}/build/config.h + ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics.h + ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics_128.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Ed25519.h ${PROJECT_SOURCE_DIR}/include/Hacl_EC_Ed25519.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Base.h @@ -141,16 +146,11 @@ set(INCLUDES ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2b_256.h ${PROJECT_SOURCE_DIR}/include/libintvector.h - ${PROJECT_SOURCE_DIR}/build/config.h ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2b_256.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2s_128.h ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2s_128.h ${PROJECT_SOURCE_DIR}/include/Hacl_Bignum256_32.h ${PROJECT_SOURCE_DIR}/include/Hacl_Bignum.h - ${PROJECT_SOURCE_DIR}/include/lib_intrinsics.h - ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics.h - ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics_128.h - ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Bignum_Base.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Bignum.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Bignum.h ${PROJECT_SOURCE_DIR}/include/Hacl_Bignum256.h @@ -182,8 +182,7 @@ set(INCLUDES ${PROJECT_SOURCE_DIR}/include/internal/Vale.h ${PROJECT_SOURCE_DIR}/include/curve25519-inline.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_P256.h - ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Spec.h - ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Spec.h + ${PROJECT_SOURCE_DIR}/include/internal/Hacl_P256_PrecompTable.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_P256.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_K256_ECDSA.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_K256_PrecompTable.h @@ -191,11 +190,10 @@ set(INCLUDES ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_K256_ECDSA.h ${PROJECT_SOURCE_DIR}/include/Hacl_EC_K256.h ${PROJECT_SOURCE_DIR}/include/Hacl_FFDHE.h + ${PROJECT_SOURCE_DIR}/include/Hacl_Spec.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Impl_FFDHE_Constants.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Hash_SHA3.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA3.h - ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Hash_SHA2.h - ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA2.h ${PROJECT_SOURCE_DIR}/include/Hacl_SHA2_Vec128.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_SHA2_Types.h ${PROJECT_SOURCE_DIR}/include/Hacl_SHA2_Vec256.h @@ -227,6 +225,8 @@ set(INCLUDES ${PROJECT_SOURCE_DIR}/include/Hacl_HPKE_P256_CP32_SHA256.h ${PROJECT_SOURCE_DIR}/include/Hacl_Frodo1344.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_SHA3.h + ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Spec.h + ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Spec.h ${PROJECT_SOURCE_DIR}/include/internal/Hacl_Frodo_KEM.h ${PROJECT_SOURCE_DIR}/include/Lib_RandomBuffer_System.h ${PROJECT_SOURCE_DIR}/include/Hacl_Frodo640.h @@ -261,13 +261,17 @@ set(PUBLIC_INCLUDES ${PROJECT_SOURCE_DIR}/include/Hacl_Curve25519_51.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Krmllib.h ${PROJECT_SOURCE_DIR}/include/Hacl_HMAC_DRBG.h - ${PROJECT_SOURCE_DIR}/include/Hacl_Spec.h + ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Types.h ${PROJECT_SOURCE_DIR}/include/Hacl_HMAC.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_SHA2.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2.h ${PROJECT_SOURCE_DIR}/include/Lib_Memzero0.h - ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Types.h + ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA2.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Curve25519_51.h + ${PROJECT_SOURCE_DIR}/include/lib_intrinsics.h + ${PROJECT_SOURCE_DIR}/build/config.h + ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics.h + ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics_128.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Ed25519.h ${PROJECT_SOURCE_DIR}/include/Hacl_EC_Ed25519.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Base.h @@ -275,15 +279,11 @@ set(PUBLIC_INCLUDES ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2b_256.h ${PROJECT_SOURCE_DIR}/include/libintvector.h - ${PROJECT_SOURCE_DIR}/build/config.h ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2b_256.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2s_128.h ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2s_128.h ${PROJECT_SOURCE_DIR}/include/Hacl_Bignum256_32.h ${PROJECT_SOURCE_DIR}/include/Hacl_Bignum.h - ${PROJECT_SOURCE_DIR}/include/lib_intrinsics.h - ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics.h - ${PROJECT_SOURCE_DIR}/include/Hacl_IntTypes_Intrinsics_128.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Bignum.h ${PROJECT_SOURCE_DIR}/include/Hacl_Bignum256.h ${PROJECT_SOURCE_DIR}/include/Hacl_Bignum32.h @@ -309,13 +309,12 @@ set(PUBLIC_INCLUDES ${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Poly1305_256.h ${PROJECT_SOURCE_DIR}/include/Hacl_Curve25519_64.h ${PROJECT_SOURCE_DIR}/include/curve25519-inline.h - ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Spec.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_P256.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_K256_ECDSA.h ${PROJECT_SOURCE_DIR}/include/Hacl_EC_K256.h ${PROJECT_SOURCE_DIR}/include/Hacl_FFDHE.h + ${PROJECT_SOURCE_DIR}/include/Hacl_Spec.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA3.h - ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA2.h ${PROJECT_SOURCE_DIR}/include/Hacl_SHA2_Vec128.h ${PROJECT_SOURCE_DIR}/include/Hacl_SHA2_Vec256.h ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA1.h @@ -344,6 +343,7 @@ set(PUBLIC_INCLUDES ${PROJECT_SOURCE_DIR}/include/Hacl_HPKE_P256_CP32_SHA256.h ${PROJECT_SOURCE_DIR}/include/Hacl_Frodo1344.h ${PROJECT_SOURCE_DIR}/include/Hacl_Hash_SHA3.h + ${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Spec.h ${PROJECT_SOURCE_DIR}/include/Lib_RandomBuffer_System.h ${PROJECT_SOURCE_DIR}/include/Hacl_Frodo640.h ${PROJECT_SOURCE_DIR}/include/Hacl_Frodo976.h diff --git a/info.txt b/info.txt index bebde94c..ac05510e 100644 --- a/info.txt +++ b/info.txt @@ -1,5 +1,5 @@ The code was generated with the following toolchain. -F* version: 355ef023467941eaf0a3ca876cd391c9f69ed78 -KaRaMeL version: 3e283efd721ceff6fc11eef4c4908662287a6ff9 -HACL* version: 9581fb9b0382aef4589e0cb76016b70b25b5add0 +F* version: e617752a1b014a16892f7d8772d62e5c234f06c1 +KaRaMeL version: 2cf2974007f4103dba5619e4eb9e3eaeefad533b +HACL* version: 86a0aed822bd80b03e4810e23518181f0edec5f6 Vale version: 0.3.19 diff --git a/ocaml/ctypes.depend b/ocaml/ctypes.depend index 86af86df..31393b5e 100644 --- a/ocaml/ctypes.depend +++ b/ocaml/ctypes.depend @@ -1,4 +1,4 @@ -CTYPES_DEPS=lib/Hacl_Streaming_Types_stubs.cmx lib/Hacl_Streaming_Types_bindings.cmx lib/Hacl_Spec_stubs.cmx lib/Hacl_Spec_bindings.cmx lib/Hacl_Hash_Blake2_stubs.cmx lib/Hacl_Hash_Blake2_bindings.cmx lib/Hacl_Hash_Blake2b_256_stubs.cmx lib/Hacl_Hash_Blake2b_256_bindings.cmx lib/Hacl_Hash_Blake2s_128_stubs.cmx lib/Hacl_Hash_Blake2s_128_bindings.cmx lib/Hacl_Hash_SHA3_stubs.cmx lib/Hacl_Hash_SHA3_bindings.cmx lib/Hacl_Hash_Base_stubs.cmx lib/Hacl_Hash_Base_bindings.cmx lib/Hacl_Hash_MD5_stubs.cmx lib/Hacl_Hash_MD5_bindings.cmx lib/Hacl_Hash_SHA1_stubs.cmx lib/Hacl_Hash_SHA1_bindings.cmx lib/Hacl_SHA2_Types_stubs.cmx lib/Hacl_SHA2_Types_bindings.cmx lib/Hacl_Hash_SHA2_stubs.cmx lib/Hacl_Hash_SHA2_bindings.cmx lib/EverCrypt_Error_stubs.cmx lib/EverCrypt_Error_bindings.cmx lib/EverCrypt_AutoConfig2_stubs.cmx lib/EverCrypt_AutoConfig2_bindings.cmx lib/EverCrypt_Hash_stubs.cmx lib/EverCrypt_Hash_bindings.cmx lib/Hacl_Chacha20_stubs.cmx lib/Hacl_Chacha20_bindings.cmx lib/Hacl_Salsa20_stubs.cmx lib/Hacl_Salsa20_bindings.cmx lib/Hacl_Bignum_Base_stubs.cmx lib/Hacl_Bignum_Base_bindings.cmx lib/Hacl_Bignum_stubs.cmx lib/Hacl_Bignum_bindings.cmx lib/Hacl_Curve25519_64_stubs.cmx lib/Hacl_Curve25519_64_bindings.cmx lib/Hacl_Bignum25519_51_stubs.cmx lib/Hacl_Bignum25519_51_bindings.cmx lib/Hacl_Curve25519_51_stubs.cmx lib/Hacl_Curve25519_51_bindings.cmx lib/Hacl_Ed25519_stubs.cmx lib/Hacl_Ed25519_bindings.cmx lib/Hacl_Poly1305_32_stubs.cmx lib/Hacl_Poly1305_32_bindings.cmx lib/Hacl_Poly1305_128_stubs.cmx lib/Hacl_Poly1305_128_bindings.cmx lib/Hacl_Poly1305_256_stubs.cmx lib/Hacl_Poly1305_256_bindings.cmx lib/Hacl_NaCl_stubs.cmx lib/Hacl_NaCl_bindings.cmx lib/Hacl_P256_stubs.cmx lib/Hacl_P256_bindings.cmx lib/Hacl_Bignum_K256_stubs.cmx lib/Hacl_Bignum_K256_bindings.cmx lib/Hacl_K256_ECDSA_stubs.cmx lib/Hacl_K256_ECDSA_bindings.cmx lib/Hacl_Frodo_KEM_stubs.cmx lib/Hacl_Frodo_KEM_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_IntTypes_Intrinsics_stubs.cmx lib/Hacl_IntTypes_Intrinsics_bindings.cmx lib/Hacl_IntTypes_Intrinsics_128_stubs.cmx lib/Hacl_IntTypes_Intrinsics_128_bindings.cmx lib/Hacl_RSAPSS_stubs.cmx lib/Hacl_RSAPSS_bindings.cmx lib/Hacl_FFDHE_stubs.cmx lib/Hacl_FFDHE_bindings.cmx lib/Hacl_Frodo640_stubs.cmx lib/Hacl_Frodo640_bindings.cmx lib/Hacl_Chacha20_Vec128_stubs.cmx lib/Hacl_Chacha20_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_128_stubs.cmx lib/Hacl_Chacha20Poly1305_128_bindings.cmx lib/Hacl_HMAC_stubs.cmx lib/Hacl_HMAC_bindings.cmx lib/Hacl_HKDF_stubs.cmx lib/Hacl_HKDF_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_bindings.cmx lib/EverCrypt_Cipher_stubs.cmx lib/EverCrypt_Cipher_bindings.cmx lib/Hacl_GenericField32_stubs.cmx lib/Hacl_GenericField32_bindings.cmx lib/Hacl_SHA2_Vec256_stubs.cmx lib/Hacl_SHA2_Vec256_bindings.cmx lib/Hacl_EC_K256_stubs.cmx lib/Hacl_EC_K256_bindings.cmx lib/Hacl_Bignum4096_stubs.cmx lib/Hacl_Bignum4096_bindings.cmx lib/Hacl_Chacha20_Vec32_stubs.cmx lib/Hacl_Chacha20_Vec32_bindings.cmx lib/EverCrypt_Ed25519_stubs.cmx lib/EverCrypt_Ed25519_bindings.cmx lib/Hacl_Bignum4096_32_stubs.cmx lib/Hacl_Bignum4096_32_bindings.cmx lib/EverCrypt_HMAC_stubs.cmx lib/EverCrypt_HMAC_bindings.cmx lib/Hacl_HMAC_DRBG_stubs.cmx lib/Hacl_HMAC_DRBG_bindings.cmx lib/EverCrypt_DRBG_stubs.cmx lib/EverCrypt_DRBG_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_bindings.cmx lib/Hacl_HPKE_P256_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP128_SHA256_bindings.cmx lib/EverCrypt_Curve25519_stubs.cmx lib/EverCrypt_Curve25519_bindings.cmx lib/Hacl_Chacha20_Vec256_stubs.cmx lib/Hacl_Chacha20_Vec256_bindings.cmx lib/Hacl_Chacha20Poly1305_256_stubs.cmx lib/Hacl_Chacha20Poly1305_256_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_bindings.cmx lib/Hacl_Frodo976_stubs.cmx lib/Hacl_Frodo976_bindings.cmx lib/Hacl_HMAC_Blake2s_128_stubs.cmx lib/Hacl_HMAC_Blake2s_128_bindings.cmx lib/Hacl_HKDF_Blake2s_128_stubs.cmx lib/Hacl_HKDF_Blake2s_128_bindings.cmx lib/Hacl_GenericField64_stubs.cmx lib/Hacl_GenericField64_bindings.cmx lib/Hacl_Frodo1344_stubs.cmx lib/Hacl_Frodo1344_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_bindings.cmx lib/Hacl_Bignum32_stubs.cmx lib/Hacl_Bignum32_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_bindings.cmx lib/Hacl_Bignum256_32_stubs.cmx lib/Hacl_Bignum256_32_bindings.cmx lib/Hacl_SHA2_Vec128_stubs.cmx lib/Hacl_SHA2_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_32_stubs.cmx lib/Hacl_Chacha20Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib/EverCrypt_Poly1305_stubs.cmx lib/EverCrypt_Poly1305_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib/Hacl_Streaming_Poly1305_32_stubs.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_bindings.cmx lib/Hacl_Streaming_Blake2_stubs.cmx lib/Hacl_Streaming_Blake2_bindings.cmx lib/Hacl_HPKE_P256_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP256_SHA256_bindings.cmx lib/Hacl_HPKE_P256_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP32_SHA256_bindings.cmx lib/Hacl_Bignum64_stubs.cmx lib/Hacl_Bignum64_bindings.cmx lib/Hacl_Frodo64_stubs.cmx lib/Hacl_Frodo64_bindings.cmx lib/Hacl_HMAC_Blake2b_256_stubs.cmx lib/Hacl_HMAC_Blake2b_256_bindings.cmx lib/Hacl_HKDF_Blake2b_256_stubs.cmx lib/Hacl_HKDF_Blake2b_256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_bindings.cmx lib/EverCrypt_HKDF_stubs.cmx lib/EverCrypt_HKDF_bindings.cmx lib/Hacl_EC_Ed25519_stubs.cmx lib/Hacl_EC_Ed25519_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_bindings.cmx lib/EverCrypt_Chacha20Poly1305_stubs.cmx lib/EverCrypt_Chacha20Poly1305_bindings.cmx lib/EverCrypt_AEAD_stubs.cmx lib/EverCrypt_AEAD_bindings.cmx lib/Hacl_Bignum256_stubs.cmx lib/Hacl_Bignum256_bindings.cmx +CTYPES_DEPS=lib/Hacl_Streaming_Types_stubs.cmx lib/Hacl_Streaming_Types_bindings.cmx lib/Hacl_Spec_stubs.cmx lib/Hacl_Spec_bindings.cmx lib/Hacl_Hash_Blake2_stubs.cmx lib/Hacl_Hash_Blake2_bindings.cmx lib/Hacl_Hash_Blake2b_256_stubs.cmx lib/Hacl_Hash_Blake2b_256_bindings.cmx lib/Hacl_Hash_Blake2s_128_stubs.cmx lib/Hacl_Hash_Blake2s_128_bindings.cmx lib/Hacl_Hash_SHA3_stubs.cmx lib/Hacl_Hash_SHA3_bindings.cmx lib/Hacl_Hash_Base_stubs.cmx lib/Hacl_Hash_Base_bindings.cmx lib/Hacl_Hash_MD5_stubs.cmx lib/Hacl_Hash_MD5_bindings.cmx lib/Hacl_Hash_SHA1_stubs.cmx lib/Hacl_Hash_SHA1_bindings.cmx lib/Hacl_SHA2_Types_stubs.cmx lib/Hacl_SHA2_Types_bindings.cmx lib/Hacl_Hash_SHA2_stubs.cmx lib/Hacl_Hash_SHA2_bindings.cmx lib/EverCrypt_Error_stubs.cmx lib/EverCrypt_Error_bindings.cmx lib/EverCrypt_AutoConfig2_stubs.cmx lib/EverCrypt_AutoConfig2_bindings.cmx lib/EverCrypt_Hash_stubs.cmx lib/EverCrypt_Hash_bindings.cmx lib/Hacl_Chacha20_stubs.cmx lib/Hacl_Chacha20_bindings.cmx lib/Hacl_Salsa20_stubs.cmx lib/Hacl_Salsa20_bindings.cmx lib/Hacl_Bignum_Base_stubs.cmx lib/Hacl_Bignum_Base_bindings.cmx lib/Hacl_Bignum_stubs.cmx lib/Hacl_Bignum_bindings.cmx lib/Hacl_Curve25519_64_stubs.cmx lib/Hacl_Curve25519_64_bindings.cmx lib/Hacl_Bignum25519_51_stubs.cmx lib/Hacl_Bignum25519_51_bindings.cmx lib/Hacl_Curve25519_51_stubs.cmx lib/Hacl_Curve25519_51_bindings.cmx lib/Hacl_Ed25519_stubs.cmx lib/Hacl_Ed25519_bindings.cmx lib/Hacl_Poly1305_32_stubs.cmx lib/Hacl_Poly1305_32_bindings.cmx lib/Hacl_Poly1305_128_stubs.cmx lib/Hacl_Poly1305_128_bindings.cmx lib/Hacl_Poly1305_256_stubs.cmx lib/Hacl_Poly1305_256_bindings.cmx lib/Hacl_NaCl_stubs.cmx lib/Hacl_NaCl_bindings.cmx lib/Hacl_P256_stubs.cmx lib/Hacl_P256_bindings.cmx lib/Hacl_Bignum_K256_stubs.cmx lib/Hacl_Bignum_K256_bindings.cmx lib/Hacl_K256_ECDSA_stubs.cmx lib/Hacl_K256_ECDSA_bindings.cmx lib/Hacl_Frodo_KEM_stubs.cmx lib/Hacl_Frodo_KEM_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_IntTypes_Intrinsics_stubs.cmx lib/Hacl_IntTypes_Intrinsics_bindings.cmx lib/Hacl_IntTypes_Intrinsics_128_stubs.cmx lib/Hacl_IntTypes_Intrinsics_128_bindings.cmx lib/Hacl_RSAPSS_stubs.cmx lib/Hacl_RSAPSS_bindings.cmx lib/Hacl_FFDHE_stubs.cmx lib/Hacl_FFDHE_bindings.cmx lib/Hacl_Frodo640_stubs.cmx lib/Hacl_Frodo640_bindings.cmx lib/Hacl_Chacha20_Vec128_stubs.cmx lib/Hacl_Chacha20_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_128_stubs.cmx lib/Hacl_Chacha20Poly1305_128_bindings.cmx lib/Hacl_HMAC_stubs.cmx lib/Hacl_HMAC_bindings.cmx lib/Hacl_HKDF_stubs.cmx lib/Hacl_HKDF_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_bindings.cmx lib/EverCrypt_Cipher_stubs.cmx lib/EverCrypt_Cipher_bindings.cmx lib/Hacl_GenericField32_stubs.cmx lib/Hacl_GenericField32_bindings.cmx lib/Hacl_SHA2_Vec256_stubs.cmx lib/Hacl_SHA2_Vec256_bindings.cmx lib/Hacl_EC_K256_stubs.cmx lib/Hacl_EC_K256_bindings.cmx lib/Hacl_Bignum4096_stubs.cmx lib/Hacl_Bignum4096_bindings.cmx lib/Hacl_Chacha20_Vec32_stubs.cmx lib/Hacl_Chacha20_Vec32_bindings.cmx lib/EverCrypt_Ed25519_stubs.cmx lib/EverCrypt_Ed25519_bindings.cmx lib/Hacl_Bignum4096_32_stubs.cmx lib/Hacl_Bignum4096_32_bindings.cmx lib/EverCrypt_HMAC_stubs.cmx lib/EverCrypt_HMAC_bindings.cmx lib/Hacl_HMAC_DRBG_stubs.cmx lib/Hacl_HMAC_DRBG_bindings.cmx lib/EverCrypt_DRBG_stubs.cmx lib/EverCrypt_DRBG_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_bindings.cmx lib/Hacl_HPKE_P256_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP128_SHA256_bindings.cmx lib/EverCrypt_Curve25519_stubs.cmx lib/EverCrypt_Curve25519_bindings.cmx lib/Hacl_Chacha20_Vec256_stubs.cmx lib/Hacl_Chacha20_Vec256_bindings.cmx lib/Hacl_Chacha20Poly1305_256_stubs.cmx lib/Hacl_Chacha20Poly1305_256_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_bindings.cmx lib/Hacl_Frodo976_stubs.cmx lib/Hacl_Frodo976_bindings.cmx lib/Hacl_HMAC_Blake2s_128_stubs.cmx lib/Hacl_HMAC_Blake2s_128_bindings.cmx lib/Hacl_HKDF_Blake2s_128_stubs.cmx lib/Hacl_HKDF_Blake2s_128_bindings.cmx lib/Hacl_GenericField64_stubs.cmx lib/Hacl_GenericField64_bindings.cmx lib/Hacl_Frodo1344_stubs.cmx lib/Hacl_Frodo1344_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_bindings.cmx lib/Hacl_Bignum32_stubs.cmx lib/Hacl_Bignum32_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_bindings.cmx lib/Hacl_Bignum256_32_stubs.cmx lib/Hacl_Bignum256_32_bindings.cmx lib/Hacl_SHA2_Vec128_stubs.cmx lib/Hacl_SHA2_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_32_stubs.cmx lib/Hacl_Chacha20Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib/EverCrypt_Poly1305_stubs.cmx lib/EverCrypt_Poly1305_bindings.cmx lib/Hacl_Streaming_Poly1305_32_stubs.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_bindings.cmx lib/Hacl_Streaming_Blake2_stubs.cmx lib/Hacl_Streaming_Blake2_bindings.cmx lib/Hacl_HPKE_P256_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP256_SHA256_bindings.cmx lib/Hacl_HPKE_P256_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP32_SHA256_bindings.cmx lib/Hacl_Bignum64_stubs.cmx lib/Hacl_Bignum64_bindings.cmx lib/Hacl_Frodo64_stubs.cmx lib/Hacl_Frodo64_bindings.cmx lib/Hacl_HMAC_Blake2b_256_stubs.cmx lib/Hacl_HMAC_Blake2b_256_bindings.cmx lib/Hacl_HKDF_Blake2b_256_stubs.cmx lib/Hacl_HKDF_Blake2b_256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_bindings.cmx lib/EverCrypt_HKDF_stubs.cmx lib/EverCrypt_HKDF_bindings.cmx lib/Hacl_EC_Ed25519_stubs.cmx lib/Hacl_EC_Ed25519_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_bindings.cmx lib/EverCrypt_Chacha20Poly1305_stubs.cmx lib/EverCrypt_Chacha20Poly1305_bindings.cmx lib/EverCrypt_AEAD_stubs.cmx lib/EverCrypt_AEAD_bindings.cmx lib/Hacl_Bignum256_stubs.cmx lib/Hacl_Bignum256_bindings.cmx lib/Hacl_Streaming_Types_bindings.cmx: lib/Hacl_Streaming_Types_bindings.cmo: lib_gen/Hacl_Streaming_Types_gen.cmx: lib/Hacl_Streaming_Types_bindings.cmx @@ -283,14 +283,14 @@ lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx: lib/Hacl_HPKE_Interface_Hacl_Imp lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmo: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmo lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmo lib_gen/Hacl_HPKE_Curve51_CP32_SHA256_gen.cmx: lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve51_CP32_SHA256_gen.exe: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_c_stubs.o lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve51_CP32_SHA256_gen.cmx -lib/EverCrypt_Poly1305_bindings.cmx: -lib/EverCrypt_Poly1305_bindings.cmo: -lib_gen/EverCrypt_Poly1305_gen.cmx: lib/EverCrypt_Poly1305_bindings.cmx -lib_gen/EverCrypt_Poly1305_gen.exe: lib/EverCrypt_Poly1305_bindings.cmx lib_gen/EverCrypt_Poly1305_gen.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmo: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmo lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmo lib_gen/Hacl_HPKE_Curve64_CP256_SHA256_gen.cmx: lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve64_CP256_SHA256_gen.exe: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_c_stubs.o lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve64_CP256_SHA256_gen.cmx +lib/EverCrypt_Poly1305_bindings.cmx: +lib/EverCrypt_Poly1305_bindings.cmo: +lib_gen/EverCrypt_Poly1305_gen.cmx: lib/EverCrypt_Poly1305_bindings.cmx +lib_gen/EverCrypt_Poly1305_gen.exe: lib/EverCrypt_Poly1305_bindings.cmx lib_gen/EverCrypt_Poly1305_gen.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmx: lib/Hacl_Streaming_Types_bindings.cmx lib/Hacl_Streaming_Types_stubs.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmo: lib/Hacl_Streaming_Types_bindings.cmo lib/Hacl_Streaming_Types_stubs.cmo lib_gen/Hacl_Streaming_Poly1305_32_gen.cmx: lib/Hacl_Streaming_Poly1305_32_bindings.cmx diff --git a/rust/Cargo.toml b/rust/Cargo.toml index 525b5208..d07b0b52 100644 --- a/rust/Cargo.toml +++ b/rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "hacl" -version = "0.0.2-dev.3" +version = "0.0.2" authors = ["Franziskus Kiefer "] edition = "2021" license = "Apache-2.0" @@ -19,7 +19,7 @@ serialization = ["serde", "serde_json"] hazmat = [] # This feature exposes raw, but safe HACL APIs for use in other libraries. Use with care. [dependencies] -hacl-sys = { version = "=0.0.2-dev.5", path = "hacl-sys" } +hacl-sys = { version = "=0.0.2", path = "hacl-sys" } rand = { version = "0.8", optional = true } rand_core = { version = "0.6", optional = true } serde_json = { version = "1.0", optional = true } @@ -29,7 +29,7 @@ serde = { version = "1.0", features = ["derive"], optional = true } hacl = { path = ".", features = ["hazmat", "random"] } serde_json = "1.0" serde = {version = "1.0", features = ["derive"]} -criterion = "0.4" +criterion = "0.5" rand = "0.8" [[bench]] diff --git a/rust/hacl-sys/Cargo.toml b/rust/hacl-sys/Cargo.toml index 2b4ce10e..ddf09861 100644 --- a/rust/hacl-sys/Cargo.toml +++ b/rust/hacl-sys/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "hacl-sys" -version = "0.0.2-dev.5" +version = "0.0.2" authors = ["Franziskus Kiefer "] edition = "2021" build = "build.rs" diff --git a/rust/hacl-sys/build.rs b/rust/hacl-sys/build.rs index 161885c0..8715130b 100644 --- a/rust/hacl-sys/build.rs +++ b/rust/hacl-sys/build.rs @@ -1,4 +1,3 @@ - use std::{env, path::Path, process::Command}; #[cfg(all(not(windows), not(nobindgen)))] @@ -184,10 +183,12 @@ fn main() { let hacl_path = if !mach_build { // Copy all of the code into out to prepare build let c_out_dir = out_dir.join("c"); - println!(" >>> Copying HACL C file"); - println!(" from {}", home_dir.join(".c").display()); - println!(" to {}", c_out_dir.display()); - copy_hacl_to_out(&c_out_dir); + if !c_out_dir.join("build").join("installed").exists() { + println!(" >>> Copying HACL C file"); + println!(" from {}", home_dir.join(".c").display()); + println!(" to {}", c_out_dir.display()); + copy_hacl_to_out(&c_out_dir); + } build_hacl_c(&c_out_dir, cross_target); c_out_dir.join("build").join("installed") @@ -206,7 +207,8 @@ fn main() { let library_name = "hacl_static"; // Set re-run trigger - println!("cargo:rerun-if-changed=wrapper.h"); + // println!("cargo:rerun-if-changed=wrapper.h"); + println!("cargo:rerun-if-changed=build.rs"); // We should re-run if the library changed. But this triggers the build // to re-run every time right now. // println!( diff --git a/rust/hacl-sys/src/bindings/bindings.rs b/rust/hacl-sys/src/bindings/bindings.rs index a286a475..35a0b157 100644 --- a/rust/hacl-sys/src/bindings/bindings.rs +++ b/rust/hacl-sys/src/bindings/bindings.rs @@ -62,10 +62,8 @@ extern "C" { mac: *mut u8, ) -> u32; } -pub type __m128i = [::std::os::raw::c_longlong; 2usize]; -pub type Lib_IntVector_Intrinsics_vec128 = __m128i; -pub type __m256i = [::std::os::raw::c_longlong; 4usize]; -pub type Lib_IntVector_Intrinsics_vec256 = __m256i; +pub type uint32x4_t = [u32; 4usize]; +pub type Lib_IntVector_Intrinsics_vec128 = uint32x4_t; extern "C" { #[doc = "Encrypt a message `m` with key `k`.\n\nThe arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption.\nNote: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory.\n\n@param k Pointer to 32 bytes of memory where the AEAD key is read from.\n@param n Pointer to 12 bytes of memory where the AEAD nonce is read from.\n@param aadlen Length of the associated data.\n@param aad Pointer to `aadlen` bytes of memory where the associated data is read from.\n\n@param mlen Length of the message.\n@param m Pointer to `mlen` bytes of memory where the message is read from.\n@param cipher Pointer to `mlen` bytes of memory where the ciphertext is written to.\n@param mac Pointer to 16 bytes of memory where the mac is written to."] pub fn Hacl_Chacha20Poly1305_256_aead_encrypt( @@ -446,6 +444,7 @@ extern "C" { -> bool; } pub type Spec_Hash_Definitions_hash_alg = u8; +pub type Hacl_Streaming_Types_error_code = u8; #[repr(C)] #[derive(Debug, Copy, Clone)] pub struct Hacl_Streaming_MD_state_32_s { @@ -486,7 +485,7 @@ extern "C" { p: *mut Hacl_Streaming_MD_state_32, input: *mut u8, input_len: u32, - ) -> u32; + ) -> Hacl_Streaming_Types_error_code; } extern "C" { #[doc = "Write the resulting hash into `dst`, an array of 32 bytes. The state remains\nvalid after a call to `finish_256`, meaning the user may feed more data into\nthe hash via `update_256`. (The finish_256 function operates on an internal copy of\nthe state and therefore does not invalidate the client-held state `p`.)"] @@ -511,7 +510,7 @@ extern "C" { p: *mut Hacl_Streaming_MD_state_32, input: *mut u8, input_len: u32, - ) -> u32; + ) -> Hacl_Streaming_Types_error_code; } extern "C" { #[doc = "Write the resulting hash into `dst`, an array of 28 bytes. The state remains\nvalid after a call to `finish_224`, meaning the user may feed more data into\nthe hash via `update_224`."] @@ -542,7 +541,7 @@ extern "C" { p: *mut Hacl_Streaming_MD_state_64, input: *mut u8, input_len: u32, - ) -> u32; + ) -> Hacl_Streaming_Types_error_code; } extern "C" { #[doc = "Write the resulting hash into `dst`, an array of 64 bytes. The state remains\nvalid after a call to `finish_512`, meaning the user may feed more data into\nthe hash via `update_512`. (The finish_512 function operates on an internal copy of\nthe state and therefore does not invalidate the client-held state `p`.)"] @@ -567,7 +566,7 @@ extern "C" { p: *mut Hacl_Streaming_MD_state_64, input: *mut u8, input_len: u32, - ) -> u32; + ) -> Hacl_Streaming_Types_error_code; } extern "C" { #[doc = "Write the resulting hash into `dst`, an array of 48 bytes. The state remains\nvalid after a call to `finish_384`, meaning the user may feed more data into\nthe hash via `update_384`."] @@ -580,46 +579,6 @@ extern "C" { #[doc = "Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes."] pub fn Hacl_Streaming_SHA2_hash_384(input: *mut u8, input_len: u32, dst: *mut u8); } -extern "C" { - pub fn Hacl_Hash_SHA2_update_multi_224(s: *mut u32, blocks: *mut u8, n_blocks: u32); -} -extern "C" { - pub fn Hacl_Hash_SHA2_update_multi_256(s: *mut u32, blocks: *mut u8, n_blocks: u32); -} -extern "C" { - pub fn Hacl_Hash_SHA2_update_multi_384(s: *mut u64, blocks: *mut u8, n_blocks: u32); -} -extern "C" { - pub fn Hacl_Hash_SHA2_update_multi_512(s: *mut u64, blocks: *mut u8, n_blocks: u32); -} -extern "C" { - pub fn Hacl_Hash_SHA2_update_last_224( - s: *mut u32, - prev_len: u64, - input: *mut u8, - input_len: u32, - ); -} -extern "C" { - pub fn Hacl_Hash_SHA2_update_last_256( - s: *mut u32, - prev_len: u64, - input: *mut u8, - input_len: u32, - ); -} -extern "C" { - pub fn Hacl_Hash_SHA2_hash_224(input: *mut u8, input_len: u32, dst: *mut u8); -} -extern "C" { - pub fn Hacl_Hash_SHA2_hash_256(input: *mut u8, input_len: u32, dst: *mut u8); -} -extern "C" { - pub fn Hacl_Hash_SHA2_hash_384(input: *mut u8, input_len: u32, dst: *mut u8); -} -extern "C" { - pub fn Hacl_Hash_SHA2_hash_512(input: *mut u8, input_len: u32, dst: *mut u8); -} extern "C" { #[doc = "Compute the public key from the private key.\n\nThe outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\nThe argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]."] pub fn Hacl_Ed25519_secret_to_public(public_key: *mut u8, private_key: *mut u8); @@ -835,21 +794,20 @@ extern "C" { p: *mut Hacl_Streaming_Keccak_state, data: *mut u8, len: u32, - ) -> u32; + ) -> Hacl_Streaming_Types_error_code; } -pub type Hacl_Streaming_Keccak_error_code = u8; extern "C" { pub fn Hacl_Streaming_Keccak_finish( s: *mut Hacl_Streaming_Keccak_state, dst: *mut u8, - ) -> Hacl_Streaming_Keccak_error_code; + ) -> Hacl_Streaming_Types_error_code; } extern "C" { pub fn Hacl_Streaming_Keccak_squeeze( s: *mut Hacl_Streaming_Keccak_state, dst: *mut u8, l: u32, - ) -> Hacl_Streaming_Keccak_error_code; + ) -> Hacl_Streaming_Types_error_code; } extern "C" { pub fn Hacl_Streaming_Keccak_block_len(s: *mut Hacl_Streaming_Keccak_state) -> u32; @@ -958,16 +916,12 @@ extern "C" { pub fn Hacl_Blake2s_128_blake2s_malloc() -> *mut Lib_IntVector_Intrinsics_vec128; } extern "C" { - pub fn Hacl_Blake2b_256_blake2b_init( - hash: *mut Lib_IntVector_Intrinsics_vec256, - kk: u32, - nn: u32, - ); + pub fn Hacl_Blake2b_256_blake2b_init(hash: *mut *mut ::std::os::raw::c_void, kk: u32, nn: u32); } extern "C" { pub fn Hacl_Blake2b_256_blake2b_update_key( - wv: *mut Lib_IntVector_Intrinsics_vec256, - hash: *mut Lib_IntVector_Intrinsics_vec256, + wv: *mut *mut ::std::os::raw::c_void, + hash: *mut *mut ::std::os::raw::c_void, kk: u32, k: *mut u8, ll: u32, @@ -977,7 +931,7 @@ extern "C" { pub fn Hacl_Blake2b_256_blake2b_finish( nn: u32, output: *mut u8, - hash: *mut Lib_IntVector_Intrinsics_vec256, + hash: *mut *mut ::std::os::raw::c_void, ); } extern "C" { @@ -993,18 +947,18 @@ extern "C" { } extern "C" { pub fn Hacl_Blake2b_256_load_state256b_from_state32( - st: *mut Lib_IntVector_Intrinsics_vec256, + st: *mut *mut ::std::os::raw::c_void, st32: *mut u64, ); } extern "C" { pub fn Hacl_Blake2b_256_store_state256b_to_state32( st32: *mut u64, - st: *mut Lib_IntVector_Intrinsics_vec256, + st: *mut *mut ::std::os::raw::c_void, ); } extern "C" { - pub fn Hacl_Blake2b_256_blake2b_malloc() -> *mut Lib_IntVector_Intrinsics_vec256; + pub fn Hacl_Blake2b_256_blake2b_malloc() -> *mut *mut ::std::os::raw::c_void; } #[repr(C)] #[derive(Debug, Copy, Clone)] diff --git a/src/Hacl_Hash_Blake2.c b/src/Hacl_Hash_Blake2.c index a5704450..6080585c 100644 --- a/src/Hacl_Hash_Blake2.c +++ b/src/Hacl_Hash_Blake2.c @@ -625,10 +625,7 @@ blake2b_update(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, uint32_t l void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash) { - uint32_t double_row = (uint32_t)64U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t b[double_row]; - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[64U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)32U; uint64_t *row0 = hash; @@ -645,7 +642,7 @@ void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash store64_le(second + i * (uint32_t)8U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U])); } /** @@ -1267,10 +1264,7 @@ blake2s_update(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, uint32_t l void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash) { - uint32_t double_row = (uint32_t)32U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t b[double_row]; - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[32U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)16U; uint32_t *row0 = hash; @@ -1287,7 +1281,7 @@ void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash store32_le(second + i * (uint32_t)4U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)32U * sizeof (b[0U])); } /** diff --git a/src/Hacl_Hash_Blake2b_256.c b/src/Hacl_Hash_Blake2b_256.c index d608d732..2761aeb1 100644 --- a/src/Hacl_Hash_Blake2b_256.c +++ b/src/Hacl_Hash_Blake2b_256.c @@ -360,10 +360,7 @@ Hacl_Blake2b_256_blake2b_finish( Lib_IntVector_Intrinsics_vec256 *hash ) { - uint32_t double_row = (uint32_t)64U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t b[double_row]; - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[64U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)32U; Lib_IntVector_Intrinsics_vec256 *row0 = hash; @@ -372,7 +369,7 @@ Hacl_Blake2b_256_blake2b_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, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U])); } /** diff --git a/src/Hacl_Hash_Blake2s_128.c b/src/Hacl_Hash_Blake2s_128.c index b6a5ce84..ce5252cc 100644 --- a/src/Hacl_Hash_Blake2s_128.c +++ b/src/Hacl_Hash_Blake2s_128.c @@ -352,10 +352,7 @@ Hacl_Blake2s_128_blake2s_finish( Lib_IntVector_Intrinsics_vec128 *hash ) { - uint32_t double_row = (uint32_t)32U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t b[double_row]; - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[32U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)16U; Lib_IntVector_Intrinsics_vec128 *row0 = hash; @@ -364,7 +361,7 @@ Hacl_Blake2s_128_blake2s_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, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)32U * sizeof (b[0U])); } /** diff --git a/src/Hacl_Hash_SHA3.c b/src/Hacl_Hash_SHA3.c index b3febdfe..42c24434 100644 --- a/src/Hacl_Hash_SHA3.c +++ b/src/Hacl_Hash_SHA3.c @@ -448,16 +448,16 @@ finish_( uint64_t *s_dst = scrut.snd.snd; uint64_t *s_src = scrut.fst.snd; memcpy(s_dst, s_src, (uint32_t)25U * sizeof (uint64_t)); - uint32_t ite0; + uint32_t ite; if (r % block_len(a) == (uint32_t)0U && r > (uint32_t)0U) { - ite0 = block_len(a); + ite = block_len(a); } else { - ite0 = r % block_len(a); + ite = r % block_len(a); } - uint8_t *buf_last = buf_1 + r - ite0; + uint8_t *buf_last = buf_1 + r - ite; uint8_t *buf_multi = buf_1; Spec_Hash_Definitions_hash_alg a1 = tmp_block_state.fst; uint64_t *s0 = tmp_block_state.snd; @@ -469,16 +469,7 @@ finish_( uint64_t *s = tmp_block_state.snd; if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256) { - uint32_t ite; - if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256) - { - ite = l; - } - else - { - ite = hash_len(a11); - } - Hacl_Impl_SHA3_squeeze(s, block_len(a11), ite, dst); + Hacl_Impl_SHA3_squeeze(s, block_len(a11), l, dst); return; } Hacl_Impl_SHA3_squeeze(s, block_len(a11), hash_len(a11), dst); diff --git a/src/msvc/Hacl_Hash_Blake2.c b/src/msvc/Hacl_Hash_Blake2.c index b3d2894e..6080585c 100644 --- a/src/msvc/Hacl_Hash_Blake2.c +++ b/src/msvc/Hacl_Hash_Blake2.c @@ -625,10 +625,7 @@ blake2b_update(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, uint32_t l void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash) { - uint32_t double_row = (uint32_t)64U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t *b = (uint8_t *)alloca(double_row * sizeof (uint8_t)); - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[64U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)32U; uint64_t *row0 = hash; @@ -645,7 +642,7 @@ void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash store64_le(second + i * (uint32_t)8U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U])); } /** @@ -1267,10 +1264,7 @@ blake2s_update(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, uint32_t l void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash) { - uint32_t double_row = (uint32_t)32U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t *b = (uint8_t *)alloca(double_row * sizeof (uint8_t)); - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[32U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)16U; uint32_t *row0 = hash; @@ -1287,7 +1281,7 @@ void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash store32_le(second + i * (uint32_t)4U, row1[i]);); uint8_t *final = b; memcpy(output, final, nn * sizeof (uint8_t)); - Lib_Memzero0_memzero(b, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)32U * sizeof (b[0U])); } /** diff --git a/src/msvc/Hacl_Hash_Blake2b_256.c b/src/msvc/Hacl_Hash_Blake2b_256.c index 3f0965e8..2761aeb1 100644 --- a/src/msvc/Hacl_Hash_Blake2b_256.c +++ b/src/msvc/Hacl_Hash_Blake2b_256.c @@ -360,10 +360,7 @@ Hacl_Blake2b_256_blake2b_finish( Lib_IntVector_Intrinsics_vec256 *hash ) { - uint32_t double_row = (uint32_t)64U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t *b = (uint8_t *)alloca(double_row * sizeof (uint8_t)); - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[64U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)32U; Lib_IntVector_Intrinsics_vec256 *row0 = hash; @@ -372,7 +369,7 @@ Hacl_Blake2b_256_blake2b_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, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U])); } /** diff --git a/src/msvc/Hacl_Hash_Blake2s_128.c b/src/msvc/Hacl_Hash_Blake2s_128.c index ad626180..ce5252cc 100644 --- a/src/msvc/Hacl_Hash_Blake2s_128.c +++ b/src/msvc/Hacl_Hash_Blake2s_128.c @@ -352,10 +352,7 @@ Hacl_Blake2s_128_blake2s_finish( Lib_IntVector_Intrinsics_vec128 *hash ) { - uint32_t double_row = (uint32_t)32U; - KRML_CHECK_SIZE(sizeof (uint8_t), double_row); - uint8_t *b = (uint8_t *)alloca(double_row * sizeof (uint8_t)); - memset(b, 0U, double_row * sizeof (uint8_t)); + uint8_t b[32U] = { 0U }; uint8_t *first = b; uint8_t *second = b + (uint32_t)16U; Lib_IntVector_Intrinsics_vec128 *row0 = hash; @@ -364,7 +361,7 @@ Hacl_Blake2s_128_blake2s_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, double_row * sizeof (b[0U])); + Lib_Memzero0_memzero(b, (uint32_t)32U * sizeof (b[0U])); } /** diff --git a/src/msvc/Hacl_Hash_SHA3.c b/src/msvc/Hacl_Hash_SHA3.c index b3febdfe..42c24434 100644 --- a/src/msvc/Hacl_Hash_SHA3.c +++ b/src/msvc/Hacl_Hash_SHA3.c @@ -448,16 +448,16 @@ finish_( uint64_t *s_dst = scrut.snd.snd; uint64_t *s_src = scrut.fst.snd; memcpy(s_dst, s_src, (uint32_t)25U * sizeof (uint64_t)); - uint32_t ite0; + uint32_t ite; if (r % block_len(a) == (uint32_t)0U && r > (uint32_t)0U) { - ite0 = block_len(a); + ite = block_len(a); } else { - ite0 = r % block_len(a); + ite = r % block_len(a); } - uint8_t *buf_last = buf_1 + r - ite0; + uint8_t *buf_last = buf_1 + r - ite; uint8_t *buf_multi = buf_1; Spec_Hash_Definitions_hash_alg a1 = tmp_block_state.fst; uint64_t *s0 = tmp_block_state.snd; @@ -469,16 +469,7 @@ finish_( uint64_t *s = tmp_block_state.snd; if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256) { - uint32_t ite; - if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256) - { - ite = l; - } - else - { - ite = hash_len(a11); - } - Hacl_Impl_SHA3_squeeze(s, block_len(a11), ite, dst); + Hacl_Impl_SHA3_squeeze(s, block_len(a11), l, dst); return; } Hacl_Impl_SHA3_squeeze(s, block_len(a11), hash_len(a11), dst); diff --git a/src/wasm/EverCrypt_Hash.wasm b/src/wasm/EverCrypt_Hash.wasm index 12254d68..843f2e85 100644 Binary files a/src/wasm/EverCrypt_Hash.wasm and b/src/wasm/EverCrypt_Hash.wasm differ diff --git a/src/wasm/Hacl_HMAC.wasm b/src/wasm/Hacl_HMAC.wasm index c0507305..b557e0f3 100644 Binary files a/src/wasm/Hacl_HMAC.wasm and b/src/wasm/Hacl_HMAC.wasm differ diff --git a/src/wasm/Hacl_Hash_Blake2.wasm b/src/wasm/Hacl_Hash_Blake2.wasm index f98c06d2..5064aa4a 100644 Binary files a/src/wasm/Hacl_Hash_Blake2.wasm and b/src/wasm/Hacl_Hash_Blake2.wasm differ diff --git a/src/wasm/Hacl_Hash_Blake2b_256.wasm b/src/wasm/Hacl_Hash_Blake2b_256.wasm index bf8b15b5..f4caa5b7 100644 Binary files a/src/wasm/Hacl_Hash_Blake2b_256.wasm and b/src/wasm/Hacl_Hash_Blake2b_256.wasm differ diff --git a/src/wasm/Hacl_Hash_Blake2s_128.wasm b/src/wasm/Hacl_Hash_Blake2s_128.wasm index 374aaf2a..d54b7190 100644 Binary files a/src/wasm/Hacl_Hash_Blake2s_128.wasm and b/src/wasm/Hacl_Hash_Blake2s_128.wasm differ diff --git a/src/wasm/Hacl_Hash_SHA3.wasm b/src/wasm/Hacl_Hash_SHA3.wasm index 22ef84a6..f9b0542d 100644 Binary files a/src/wasm/Hacl_Hash_SHA3.wasm and b/src/wasm/Hacl_Hash_SHA3.wasm differ diff --git a/src/wasm/Hacl_Streaming_Blake2.wasm b/src/wasm/Hacl_Streaming_Blake2.wasm index d5dd37a8..ff2f0e69 100644 Binary files a/src/wasm/Hacl_Streaming_Blake2.wasm and b/src/wasm/Hacl_Streaming_Blake2.wasm differ diff --git a/src/wasm/INFO.txt b/src/wasm/INFO.txt index c3cbc8e7..0288bd71 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: 504c21f3c02a82d5ed2d2db746245157c995e9e5 -KaRaMeL version: 2cf2974007f4103dba5619e4eb9e3eaeefad533b +F* version: e617752a1b014a16892f7d8772d62e5c234f06c1 +Karamel version: 2cf2974007f4103dba5619e4eb9e3eaeefad533b Vale version: 0.3.19