merge and update

* merge branch 'main' into pnmadelaine-update

* update to HACL* cfd50bcf32693f7b3ad210e39de9371d1c242101

* restore ocaml/lib/Lib_RandomBuffer_System_bindings.ml

* update info.txt

* fix tests

* update rust bindings

.github/workflows/gh-pages.yml

@@ -127,6 +127,16 @@ jobs:
           mkdir -p build/js
           cp -r src/wasm/doc/out build/js/main
 
+      - name: Build | Rust Docs
+        run: |
+          mkdir -p build/rust
+          cd rust/hacl-sys
+          cargo doc --no-deps
+          cp -r target/doc ../../build/rust/main
+          cd ../
+          cargo doc --no-deps --all-features
+          cp -r target/doc/* ../build/rust/main
+
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v1
         with:

CMakeLists.txt

@@ -251,7 +251,7 @@ if(TOOLCHAIN_CAN_COMPILE_VEC256)
         target_include_directories(hacl_vec256 PRIVATE)
 
         # We really should only get here on x86 architectures. But let's make sure.
-        if(CMAKE_SYSTEM_PROCESSOR MATCHES "i386|i586|i686|i86pc|ia32|x86_64|amd64|AMD64")
+        if(CMAKE_SYSTEM_PROCESSOR MATCHES "i386|i586|i686|i86pc|ia32|x86|x86_64|amd64|AMD64")
             if(MSVC)
                 target_compile_options(hacl_vec256 PRIVATE
                     /arch:AVX
@@ -302,7 +302,7 @@ if(CMAKE_SYSTEM_PROCESSOR MATCHES "x86_64|amd64|AMD64")
     set(HACL_TARGET_ARCHITECTURE ${HACL_ARCHITECTURE_X64})
 
 # x86
-elseif(CMAKE_SYSTEM_PROCESSOR MATCHES "i386|i586|i686|i86pc|ia32")
+elseif(CMAKE_SYSTEM_PROCESSOR MATCHES "i386|i586|i686|i86pc|ia32|x86")
     message(STATUS "Detected an x86 architecture")
     set(ARCHITECTURE intel)
     set(HACL_TARGET_ARCHITECTURE ${HACL_ARCHITECTURE_X86})
@@ -473,16 +473,17 @@ if(ENABLE_BENCHMARKS)
     # We need gtest as well
     FetchContent_Declare(googletest
 	DOWNLOAD_EXTRACT_TIMESTAMP TRUE
-        URL https://github.com/google/googletest/archive/refs/tags/release-1.11.0.zip
+        URL https://github.com/google/googletest/archive/refs/tags/v1.13.0.zip
     )
 
     # For Windows: Prevent overriding the parent project's compiler/linker settings
     set(gtest_force_shared_crt ON CACHE BOOL "" FORCE)
     FetchContent_MakeAvailable(googletest)
 
     FetchContent_Populate(benchmark
-        GIT_REPOSITORY  https://github.com/google/benchmark
-        GIT_TAG         v1.7.0
+        GIT_REPOSITORY  https://github.com/google/benchmark.git
+        # The latest release 1.7.1 is broken due to https://github.com/google/benchmark/pull/1517
+        GIT_TAG         b177433f3ee2513b1075140c723d73ab8901790f
     )
     add_subdirectory(${benchmark_SOURCE_DIR} ${benchmark_BINARY_DIR})
 

benchmarks/blake.cc

@@ -160,7 +160,7 @@ HACL_blake2b_32_streaming(benchmark::State& state)
     Hacl_Hash_Blake2b_state_t* ctx = Hacl_Hash_Blake2b_malloc();
 
     // Update
-    for (auto chunk : chunk(input, 7)) {
+    for (auto chunk : chunk(input, chunk_len)) {
       Hacl_Hash_Blake2b_update(ctx, (uint8_t*)chunk.data(), chunk.size());
     }
 
@@ -188,7 +188,7 @@ HACL_blake2b_vec256_streaming(benchmark::State& state)
     Hacl_Hash_Blake2b_Simd256_state_t* ctx = Hacl_Hash_Blake2b_Simd256_malloc();
 
     // Update
-    for (auto chunk : chunk(input, 7)) {
+    for (auto chunk : chunk(input, chunk_len)) {
       Hacl_Hash_Blake2b_Simd256_update(
         ctx, (uint8_t*)chunk.data(), chunk.size());
     }
@@ -213,7 +213,7 @@ EverCrypt_blake2b_streaming(benchmark::State& state)
       EverCrypt_Hash_Incremental_malloc(Spec_Hash_Definitions_Blake2B);
 
     // Update
-    for (auto chunk : chunk(input, 7)) {
+    for (auto chunk : chunk(input, chunk_len)) {
       EverCrypt_Hash_Incremental_update(ctx, chunk.data(), chunk.size());
     }
 
@@ -359,7 +359,7 @@ HACL_blake2s_32_streaming(benchmark::State& state)
     Hacl_Hash_Blake2s_state_t* ctx = Hacl_Hash_Blake2s_malloc();
 
     // Update
-    for (auto chunk : chunk(input, 7)) {
+    for (auto chunk : chunk(input, chunk_len)) {
       Hacl_Hash_Blake2s_update(ctx, (uint8_t*)chunk.data(), chunk.size());
     }
 
@@ -387,7 +387,7 @@ HACL_blake2s_vec128_streaming(benchmark::State& state)
     Hacl_Hash_Blake2s_Simd128_state_t* ctx = Hacl_Hash_Blake2s_Simd128_malloc();
 
     // Update
-    for (auto chunk : chunk(input, 7)) {
+    for (auto chunk : chunk(input, chunk_len)) {
       Hacl_Hash_Blake2s_Simd128_update(
         ctx, (uint8_t*)chunk.data(), chunk.size());
     }
@@ -412,7 +412,7 @@ EverCrypt_blake2s_streaming(benchmark::State& state)
       EverCrypt_Hash_Incremental_malloc(Spec_Hash_Definitions_Blake2S);
 
     // Update
-    for (auto chunk : chunk(input, 7)) {
+    for (auto chunk : chunk(input, chunk_len)) {
       EverCrypt_Hash_Incremental_update(ctx, chunk.data(), chunk.size());
     }
 

config/default_config.cmake

@@ -185,7 +185,8 @@ set(INCLUDES
 	${PROJECT_SOURCE_DIR}/include/Hacl_EC_K256.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_FFDHE.h
 	${PROJECT_SOURCE_DIR}/include/internal/Hacl_Impl_FFDHE_Constants.h
-	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_SHA3.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
@@ -218,6 +219,7 @@ set(INCLUDES
 	${PROJECT_SOURCE_DIR}/include/Hacl_HPKE_P256_CP128_SHA256.h
 	${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_Frodo_KEM.h
 	${PROJECT_SOURCE_DIR}/include/Lib_RandomBuffer_System.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Frodo640.h
@@ -299,7 +301,7 @@ set(PUBLIC_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_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/Hacl_SHA2_Vec128.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_SHA2_Vec256.h
@@ -328,6 +330,7 @@ set(PUBLIC_INCLUDES
 	${PROJECT_SOURCE_DIR}/include/Hacl_HPKE_P256_CP128_SHA256.h
 	${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/Lib_RandomBuffer_System.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Frodo640.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Frodo976.h

docs/book/src/SUMMARY.md

@@ -30,6 +30,7 @@
   - [Build Process](./developers/build-process.md)
     - [Rust](./developers/rust-build.md)
     - [OCaml](./developers/ocaml-build.md)
+    - [JavaScript](./developers/js-build.md)
   - [Continuous Integration](./developers/ci.md)
   - [Documentation](./developers/documentation.md)
     - [OCaml](./developers/ocaml-docs.md)

docs/book/src/developers/js-build.md

@@ -0,0 +1,40 @@
+# JavaScript
+
+## Building, testing, and installing the `hacl-wasm` npm package
+
+The package directory can be put together using a script:
+
+```bash
+./npm.sh
+cd npm
+```
+
+Tests can be run with:
+
+```bash
+node api_test.js
+```
+
+The package can be installed with:
+
+```bash
+npm install
+```
+
+
+## Publishing a new version of the `hacl-wasm` package to npm
+
+Assuming all the steps above ran successfully, a new version of the package
+can be published on npm. First, update the version number in `package.json`
+and propagate it using `npm install`.
+
+A tag `js-vX.X.X` should be created with the new version of the package.
+
+The package can then be published with:
+
+```bash
+npm publish
+```
+
+This last step requires having logged in to npm and having the correct
+access rights.

docs/book/src/hacl-ocaml/readme.md

@@ -11,6 +11,7 @@ See [Changes.md] for changes between the versions.
 
 | Version | Package 📦    | Docs 📚       |
 | ------- | ------------- | ------------- |
+| 0.7.0   | [opam v0.7.0] | [Docs v0.7.0] |
 | 0.6.2   | [opam v0.6.2] | [Docs v0.6.2] |
 | 0.6.1   | [opam v0.6.1] | [Docs v0.6.1] |
 | 0.6.0   | [opam v0.6.0] | [Docs v0.6.0] |
@@ -21,7 +22,9 @@ See [Changes.md] for changes between the versions.
 [opam v0.6.0]: https://opam.ocaml.org/packages/hacl-star/hacl-star.0.6.0/
 [opam v0.6.1]: https://opam.ocaml.org/packages/hacl-star/hacl-star.0.6.1/
 [opam v0.6.2]: https://opam.ocaml.org/packages/hacl-star/hacl-star.0.6.2/
+[opam v0.7.0]: https://opam.ocaml.org/packages/hacl-star/hacl-star.0.7.0/
 [docs v0.5.0]: https://tech.cryspen.com/hacl-packages/ocaml/ocaml-v0.5.0/index.html
 [docs v0.6.0]: https://tech.cryspen.com/hacl-packages/ocaml/ocaml-v0.6.0/index.html
 [docs v0.6.1]: https://tech.cryspen.com/hacl-packages/ocaml/ocaml-v0.6.1/index.html
 [docs v0.6.2]: https://tech.cryspen.com/hacl-packages/ocaml/ocaml-v0.6.2/index.html
+[docs v0.7.0]: https://tech.cryspen.com/hacl-packages/ocaml/ocaml-v0.7.0/index.html

docs/book/src/news.md

@@ -5,7 +5,24 @@ This is not authoritative. Please see the [CHANGELOG] for released changes.
 
 ## February 2023
 
-[Git changes](https://github.com/cryspen/hacl-packages/compare/1077e5f8be4b1a1b0c6987c8c105eabb4e02c54a...main)
+[Git changes](https://github.com/cryspen/hacl-packages/compare/cc6a47829626e9b4a1dab892b1bde96990fde2b2...main)
+
+## March 2023
+
+[Git changes](https://github.com/cryspen/hacl-packages/compare/fb7535487cd852bda3362977dda6331bd3143fe1...cc6a47829626e9b4a1dab892b1bde96990fde2b2)
+
+### Added
+
+- Rust low-level APIs
+- OCaml v0.7.0
+
+### Fixed
+
+- FreeBSD build
+
+## February 2023
+
+[Git changes](https://github.com/cryspen/hacl-packages/compare/1077e5f8be4b1a1b0c6987c8c105eabb4e02c54a...fb7535487cd852bda3362977dda6331bd3143fe1)
 
 ### Changed
 

include/EverCrypt_Hash.h

@@ -135,8 +135,14 @@ EverCrypt_Hash_Incremental_hash(
 
 #define SHA2_512_HASH_LEN ((uint32_t)64U)
 
+#define SHA3_224_HASH_LEN ((uint32_t)28U)
+
 #define SHA3_256_HASH_LEN ((uint32_t)32U)
 
+#define SHA3_384_HASH_LEN ((uint32_t)48U)
+
+#define SHA3_512_HASH_LEN ((uint32_t)64U)
+
 #define BLAKE2S_HASH_LEN ((uint32_t)32U)
 
 #define BLAKE2B_HASH_LEN ((uint32_t)64U)

include/Hacl_Chacha20Poly1305_128.h

@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_MAC_Poly1305_Simd128.h"
 #include "Hacl_Chacha20_Vec128.h"
 
 /**

include/Hacl_Chacha20Poly1305_256.h

@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_MAC_Poly1305_Simd256.h"
 #include "Hacl_Chacha20_Vec256.h"
 
 /**

include/Hacl_Chacha20Poly1305_32.h

@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_MAC_Poly1305.h"
 #include "Hacl_Chacha20.h"
 
 /**

include/Hacl_Hash_Base.h

@@ -47,6 +47,8 @@ uint32_t Hacl_Hash_Definitions_hash_len(Spec_Hash_Definitions_hash_alg a);
 
 typedef uint8_t *Hacl_Hash_Definitions_hash_t;
 
+typedef Spec_Hash_Definitions_hash_alg Hacl_Hash_Definitions_const_impl;
+
 #if defined(__cplusplus)
 }
 #endif

include/Hacl_Hash_Blake2b.h

@@ -38,61 +38,6 @@ extern "C" {
 #include "Lib_Memzero0.h"
 #include "Hacl_Krmllib.h"
 
-void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn);
-
-void
-Hacl_Hash_Blake2b_update_key(
-  uint64_t *wv,
-  uint64_t *hash,
-  uint32_t kk,
-  uint8_t *k,
-  uint32_t ll
-);
-
-void
-Hacl_Hash_Blake2b_update_multi(
-  uint32_t len,
-  uint64_t *wv,
-  uint64_t *hash,
-  FStar_UInt128_uint128 prev,
-  uint8_t *blocks,
-  uint32_t nb
-);
-
-void
-Hacl_Hash_Blake2b_update_last(
-  uint32_t len,
-  uint64_t *wv,
-  uint64_t *hash,
-  FStar_UInt128_uint128 prev,
-  uint32_t rem,
-  uint8_t *d
-);
-
-void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash);
-
-/**
-Write the BLAKE2b digest of message `input` using key `key` into `output`.
-
-@param output Pointer to `output_len` bytes of memory where the digest is written to.
-@param output_len Length of the to-be-generated digest with 1 <= `output_len` <= 64.
-@param input Pointer to `input_len` bytes of memory where the input message is read from.
-@param input_len Length of the input message.
-@param key Pointer to `key_len` bytes of memory where the key is read from.
-@param key_len Length of the key. Can be 0.
-*/
-void
-Hacl_Hash_Blake2b_hash_with_key(
-  uint8_t *output,
-  uint32_t output_len,
-  uint8_t *input,
-  uint32_t input_len,
-  uint8_t *key,
-  uint32_t key_len
-);
-
-uint64_t *Hacl_Hash_Blake2b_malloc_with_key(void);
-
 typedef struct Hacl_Hash_Blake2b_block_state_t_s
 {
   uint64_t *fst;
@@ -134,6 +79,26 @@ void Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *state, uint8_t *output)
 */
 void Hacl_Hash_Blake2b_free(Hacl_Hash_Blake2b_state_t *state);
 
+/**
+Write the BLAKE2b digest of message `input` using key `key` into `output`.
+
+@param output Pointer to `output_len` bytes of memory where the digest is written to.
+@param output_len Length of the to-be-generated digest with 1 <= `output_len` <= 64.
+@param input Pointer to `input_len` bytes of memory where the input message is read from.
+@param input_len Length of the input message.
+@param key Pointer to `key_len` bytes of memory where the key is read from.
+@param key_len Length of the key. Can be 0.
+*/
+void
+Hacl_Hash_Blake2b_hash_with_key(
+  uint8_t *output,
+  uint32_t output_len,
+  uint8_t *input,
+  uint32_t input_len,
+  uint8_t *key,
+  uint32_t key_len
+);
+
 #if defined(__cplusplus)
 }
 #endif