Assume Vec256 feature

emillon · Mar 4, 2022 · f96e3b9 · f96e3b9
1 parent 1dd3885
commit f96e3b9
Show file tree

Hide file tree

Showing 5 changed files with 81 additions and 3 deletions.
diff --git a/AutoConfig2.ml b/AutoConfig2.ml
@@ -18,7 +18,7 @@ let has_feature = function
   | AES_NI -> everCrypt_AutoConfig2_has_aesni ()
   | PCLMULQDQ -> everCrypt_AutoConfig2_has_pclmulqdq ()
   | VEC128 -> everCrypt_AutoConfig2_has_vec128 ()
-  | VEC256 -> false
+  | VEC256 -> everCrypt_AutoConfig2_has_vec256 ()
   | BMI2 -> everCrypt_AutoConfig2_has_bmi2 ()
   | ADX -> everCrypt_AutoConfig2_has_adx ()
   | SSE -> everCrypt_AutoConfig2_has_sse ()

diff --git a/dune.inc b/dune.inc
@@ -12,6 +12,8 @@ Hacl_Hash_Base_stubs
 Hacl_Hash_Base_bindings
 Hacl_Hash_Blake2_stubs
 Hacl_Hash_Blake2_bindings
+Hacl_Hash_Blake2b_256_stubs
+Hacl_Hash_Blake2b_256_bindings
 Hacl_Hash_Blake2s_128_stubs
 Hacl_Hash_Blake2s_128_bindings
 Hacl_Hash_MD5_stubs
@@ -48,6 +50,8 @@ Hacl_Poly1305_32_stubs
 Hacl_Poly1305_32_bindings
 Hacl_Poly1305_128_stubs
 Hacl_Poly1305_128_bindings
+Hacl_Poly1305_256_stubs
+Hacl_Poly1305_256_bindings
 Hacl_NaCl_stubs
 Hacl_NaCl_bindings
 EverCrypt_Error_stubs
@@ -84,6 +88,8 @@ Hacl_GenericField32_stubs
 Hacl_GenericField32_bindings
 Hacl_Bignum256_stubs
 Hacl_Bignum256_bindings
+Hacl_SHA2_Vec256_stubs
+Hacl_SHA2_Vec256_bindings
 Hacl_Bignum4096_stubs
 Hacl_Bignum4096_bindings
 Hacl_Chacha20_Vec32_stubs
@@ -94,6 +100,12 @@ Hacl_Bignum4096_32_stubs
 Hacl_Bignum4096_32_bindings
 Hacl_HPKE_P256_CP128_SHA256_stubs
 Hacl_HPKE_P256_CP128_SHA256_bindings
+Hacl_Chacha20_Vec256_stubs
+Hacl_Chacha20_Vec256_bindings
+Hacl_Chacha20Poly1305_256_stubs
+Hacl_Chacha20Poly1305_256_bindings
+Hacl_HPKE_Curve51_CP256_SHA512_stubs
+Hacl_HPKE_Curve51_CP256_SHA512_bindings
 Hacl_SHA2_Scalar32_stubs
 Hacl_SHA2_Scalar32_bindings
 Hacl_Frodo976_stubs
@@ -122,6 +134,8 @@ Hacl_Streaming_Poly1305_32_stubs
 Hacl_Streaming_Poly1305_32_bindings
 Hacl_HPKE_Curve51_CP32_SHA512_stubs
 Hacl_HPKE_Curve51_CP32_SHA512_bindings
+Hacl_HPKE_P256_CP256_SHA256_stubs
+Hacl_HPKE_P256_CP256_SHA256_bindings
 Hacl_HPKE_P256_CP32_SHA256_stubs
 Hacl_HPKE_P256_CP32_SHA256_bindings
 Hacl_Bignum64_stubs
@@ -132,8 +146,14 @@ Hacl_Streaming_SHA1_stubs
 Hacl_Streaming_SHA1_bindings
 Hacl_Streaming_MD5_stubs
 Hacl_Streaming_MD5_bindings
+Hacl_HMAC_Blake2b_256_stubs
+Hacl_HMAC_Blake2b_256_bindings
+Hacl_HKDF_Blake2b_256_stubs
+Hacl_HKDF_Blake2b_256_bindings
 Hacl_EC_Ed25519_stubs
 Hacl_EC_Ed25519_bindings
+Hacl_HPKE_Curve51_CP256_SHA256_stubs
+Hacl_HPKE_Curve51_CP256_SHA256_bindings
 EverCrypt_Chacha20Poly1305_stubs
 EverCrypt_Chacha20Poly1305_bindings
 EverCrypt_AEAD_stubs
@@ -172,6 +192,8 @@ Hacl_Hash_Base_stubs.ml
 Hacl_Hash_Base_bindings.ml
 Hacl_Hash_Blake2_stubs.ml
 Hacl_Hash_Blake2_bindings.ml
+Hacl_Hash_Blake2b_256_stubs.ml
+Hacl_Hash_Blake2b_256_bindings.ml
 Hacl_Hash_Blake2s_128_stubs.ml
 Hacl_Hash_Blake2s_128_bindings.ml
 Hacl_Hash_MD5_stubs.ml
@@ -208,6 +230,8 @@ Hacl_Poly1305_32_stubs.ml
 Hacl_Poly1305_32_bindings.ml
 Hacl_Poly1305_128_stubs.ml
 Hacl_Poly1305_128_bindings.ml
+Hacl_Poly1305_256_stubs.ml
+Hacl_Poly1305_256_bindings.ml
 Hacl_NaCl_stubs.ml
 Hacl_NaCl_bindings.ml
 EverCrypt_Error_stubs.ml
@@ -244,6 +268,8 @@ Hacl_GenericField32_stubs.ml
 Hacl_GenericField32_bindings.ml
 Hacl_Bignum256_stubs.ml
 Hacl_Bignum256_bindings.ml
+Hacl_SHA2_Vec256_stubs.ml
+Hacl_SHA2_Vec256_bindings.ml
 Hacl_Bignum4096_stubs.ml
 Hacl_Bignum4096_bindings.ml
 Hacl_Chacha20_Vec32_stubs.ml
@@ -254,6 +280,12 @@ Hacl_Bignum4096_32_stubs.ml
 Hacl_Bignum4096_32_bindings.ml
 Hacl_HPKE_P256_CP128_SHA256_stubs.ml
 Hacl_HPKE_P256_CP128_SHA256_bindings.ml
+Hacl_Chacha20_Vec256_stubs.ml
+Hacl_Chacha20_Vec256_bindings.ml
+Hacl_Chacha20Poly1305_256_stubs.ml
+Hacl_Chacha20Poly1305_256_bindings.ml
+Hacl_HPKE_Curve51_CP256_SHA512_stubs.ml
+Hacl_HPKE_Curve51_CP256_SHA512_bindings.ml
 Hacl_SHA2_Scalar32_stubs.ml
 Hacl_SHA2_Scalar32_bindings.ml
 Hacl_Frodo976_stubs.ml
@@ -282,6 +314,8 @@ Hacl_Streaming_Poly1305_32_stubs.ml
 Hacl_Streaming_Poly1305_32_bindings.ml
 Hacl_HPKE_Curve51_CP32_SHA512_stubs.ml
 Hacl_HPKE_Curve51_CP32_SHA512_bindings.ml
+Hacl_HPKE_P256_CP256_SHA256_stubs.ml
+Hacl_HPKE_P256_CP256_SHA256_bindings.ml
 Hacl_HPKE_P256_CP32_SHA256_stubs.ml
 Hacl_HPKE_P256_CP32_SHA256_bindings.ml
 Hacl_Bignum64_stubs.ml
@@ -292,8 +326,14 @@ Hacl_Streaming_SHA1_stubs.ml
 Hacl_Streaming_SHA1_bindings.ml
 Hacl_Streaming_MD5_stubs.ml
 Hacl_Streaming_MD5_bindings.ml
+Hacl_HMAC_Blake2b_256_stubs.ml
+Hacl_HMAC_Blake2b_256_bindings.ml
+Hacl_HKDF_Blake2b_256_stubs.ml
+Hacl_HKDF_Blake2b_256_bindings.ml
 Hacl_EC_Ed25519_stubs.ml
 Hacl_EC_Ed25519_bindings.ml
+Hacl_HPKE_Curve51_CP256_SHA256_stubs.ml
+Hacl_HPKE_Curve51_CP256_SHA256_bindings.ml
 EverCrypt_Chacha20Poly1305_stubs.ml
 EverCrypt_Chacha20Poly1305_bindings.ml
 EverCrypt_AEAD_stubs.ml
@@ -336,6 +376,8 @@ Lib_RandomBuffer_System_bindings.ml
 (copy raw/lib/Hacl_Hash_Base_bindings.ml Hacl_Hash_Base_bindings.ml)
 (copy raw/lib/Hacl_Hash_Blake2_stubs.ml Hacl_Hash_Blake2_stubs.ml)
 (copy raw/lib/Hacl_Hash_Blake2_bindings.ml Hacl_Hash_Blake2_bindings.ml)
+(copy raw/lib/Hacl_Hash_Blake2b_256_stubs.ml Hacl_Hash_Blake2b_256_stubs.ml)
+(copy raw/lib/Hacl_Hash_Blake2b_256_bindings.ml Hacl_Hash_Blake2b_256_bindings.ml)
 (copy raw/lib/Hacl_Hash_Blake2s_128_stubs.ml Hacl_Hash_Blake2s_128_stubs.ml)
 (copy raw/lib/Hacl_Hash_Blake2s_128_bindings.ml Hacl_Hash_Blake2s_128_bindings.ml)
 (copy raw/lib/Hacl_Hash_MD5_stubs.ml Hacl_Hash_MD5_stubs.ml)
@@ -372,6 +414,8 @@ Lib_RandomBuffer_System_bindings.ml
 (copy raw/lib/Hacl_Poly1305_32_bindings.ml Hacl_Poly1305_32_bindings.ml)
 (copy raw/lib/Hacl_Poly1305_128_stubs.ml Hacl_Poly1305_128_stubs.ml)
 (copy raw/lib/Hacl_Poly1305_128_bindings.ml Hacl_Poly1305_128_bindings.ml)
+(copy raw/lib/Hacl_Poly1305_256_stubs.ml Hacl_Poly1305_256_stubs.ml)
+(copy raw/lib/Hacl_Poly1305_256_bindings.ml Hacl_Poly1305_256_bindings.ml)
 (copy raw/lib/Hacl_NaCl_stubs.ml Hacl_NaCl_stubs.ml)
 (copy raw/lib/Hacl_NaCl_bindings.ml Hacl_NaCl_bindings.ml)
 (copy raw/lib/EverCrypt_Error_stubs.ml EverCrypt_Error_stubs.ml)
@@ -408,6 +452,8 @@ Lib_RandomBuffer_System_bindings.ml
 (copy raw/lib/Hacl_GenericField32_bindings.ml Hacl_GenericField32_bindings.ml)
 (copy raw/lib/Hacl_Bignum256_stubs.ml Hacl_Bignum256_stubs.ml)
 (copy raw/lib/Hacl_Bignum256_bindings.ml Hacl_Bignum256_bindings.ml)
+(copy raw/lib/Hacl_SHA2_Vec256_stubs.ml Hacl_SHA2_Vec256_stubs.ml)
+(copy raw/lib/Hacl_SHA2_Vec256_bindings.ml Hacl_SHA2_Vec256_bindings.ml)
 (copy raw/lib/Hacl_Bignum4096_stubs.ml Hacl_Bignum4096_stubs.ml)
 (copy raw/lib/Hacl_Bignum4096_bindings.ml Hacl_Bignum4096_bindings.ml)
 (copy raw/lib/Hacl_Chacha20_Vec32_stubs.ml Hacl_Chacha20_Vec32_stubs.ml)
@@ -418,6 +464,12 @@ Lib_RandomBuffer_System_bindings.ml
 (copy raw/lib/Hacl_Bignum4096_32_bindings.ml Hacl_Bignum4096_32_bindings.ml)
 (copy raw/lib/Hacl_HPKE_P256_CP128_SHA256_stubs.ml Hacl_HPKE_P256_CP128_SHA256_stubs.ml)
 (copy raw/lib/Hacl_HPKE_P256_CP128_SHA256_bindings.ml Hacl_HPKE_P256_CP128_SHA256_bindings.ml)
+(copy raw/lib/Hacl_Chacha20_Vec256_stubs.ml Hacl_Chacha20_Vec256_stubs.ml)
+(copy raw/lib/Hacl_Chacha20_Vec256_bindings.ml Hacl_Chacha20_Vec256_bindings.ml)
+(copy raw/lib/Hacl_Chacha20Poly1305_256_stubs.ml Hacl_Chacha20Poly1305_256_stubs.ml)
+(copy raw/lib/Hacl_Chacha20Poly1305_256_bindings.ml Hacl_Chacha20Poly1305_256_bindings.ml)
+(copy raw/lib/Hacl_HPKE_Curve51_CP256_SHA512_stubs.ml Hacl_HPKE_Curve51_CP256_SHA512_stubs.ml)
+(copy raw/lib/Hacl_HPKE_Curve51_CP256_SHA512_bindings.ml Hacl_HPKE_Curve51_CP256_SHA512_bindings.ml)
 (copy raw/lib/Hacl_SHA2_Scalar32_stubs.ml Hacl_SHA2_Scalar32_stubs.ml)
 (copy raw/lib/Hacl_SHA2_Scalar32_bindings.ml Hacl_SHA2_Scalar32_bindings.ml)
 (copy raw/lib/Hacl_Frodo976_stubs.ml Hacl_Frodo976_stubs.ml)
@@ -446,6 +498,8 @@ Lib_RandomBuffer_System_bindings.ml
 (copy raw/lib/Hacl_Streaming_Poly1305_32_bindings.ml Hacl_Streaming_Poly1305_32_bindings.ml)
 (copy raw/lib/Hacl_HPKE_Curve51_CP32_SHA512_stubs.ml Hacl_HPKE_Curve51_CP32_SHA512_stubs.ml)
 (copy raw/lib/Hacl_HPKE_Curve51_CP32_SHA512_bindings.ml Hacl_HPKE_Curve51_CP32_SHA512_bindings.ml)
+(copy raw/lib/Hacl_HPKE_P256_CP256_SHA256_stubs.ml Hacl_HPKE_P256_CP256_SHA256_stubs.ml)
+(copy raw/lib/Hacl_HPKE_P256_CP256_SHA256_bindings.ml Hacl_HPKE_P256_CP256_SHA256_bindings.ml)
 (copy raw/lib/Hacl_HPKE_P256_CP32_SHA256_stubs.ml Hacl_HPKE_P256_CP32_SHA256_stubs.ml)
 (copy raw/lib/Hacl_HPKE_P256_CP32_SHA256_bindings.ml Hacl_HPKE_P256_CP32_SHA256_bindings.ml)
 (copy raw/lib/Hacl_Bignum64_stubs.ml Hacl_Bignum64_stubs.ml)
@@ -456,8 +510,14 @@ Lib_RandomBuffer_System_bindings.ml
 (copy raw/lib/Hacl_Streaming_SHA1_bindings.ml Hacl_Streaming_SHA1_bindings.ml)
 (copy raw/lib/Hacl_Streaming_MD5_stubs.ml Hacl_Streaming_MD5_stubs.ml)
 (copy raw/lib/Hacl_Streaming_MD5_bindings.ml Hacl_Streaming_MD5_bindings.ml)
+(copy raw/lib/Hacl_HMAC_Blake2b_256_stubs.ml Hacl_HMAC_Blake2b_256_stubs.ml)
+(copy raw/lib/Hacl_HMAC_Blake2b_256_bindings.ml Hacl_HMAC_Blake2b_256_bindings.ml)
+(copy raw/lib/Hacl_HKDF_Blake2b_256_stubs.ml Hacl_HKDF_Blake2b_256_stubs.ml)
+(copy raw/lib/Hacl_HKDF_Blake2b_256_bindings.ml Hacl_HKDF_Blake2b_256_bindings.ml)
 (copy raw/lib/Hacl_EC_Ed25519_stubs.ml Hacl_EC_Ed25519_stubs.ml)
 (copy raw/lib/Hacl_EC_Ed25519_bindings.ml Hacl_EC_Ed25519_bindings.ml)
+(copy raw/lib/Hacl_HPKE_Curve51_CP256_SHA256_stubs.ml Hacl_HPKE_Curve51_CP256_SHA256_stubs.ml)
+(copy raw/lib/Hacl_HPKE_Curve51_CP256_SHA256_bindings.ml Hacl_HPKE_Curve51_CP256_SHA256_bindings.ml)
 (copy raw/lib/EverCrypt_Chacha20Poly1305_stubs.ml EverCrypt_Chacha20Poly1305_stubs.ml)
 (copy raw/lib/EverCrypt_Chacha20Poly1305_bindings.ml EverCrypt_Chacha20Poly1305_bindings.ml)
 (copy raw/lib/EverCrypt_AEAD_stubs.ml EverCrypt_AEAD_stubs.ml)

diff --git a/gen_dune_rules.ml b/gen_dune_rules.ml
@@ -13,6 +13,7 @@ let modules =
   [ "Hacl_Spec"
   ; "Hacl_Hash_Base"
   ; "Hacl_Hash_Blake2"
+  ; "Hacl_Hash_Blake2b_256"
   ; "Hacl_Hash_Blake2s_128"
   ; "Hacl_Hash_MD5"
   ; "Hacl_Hash_SHA1"
@@ -31,6 +32,7 @@ let modules =
   ; "Hacl_Ed25519"
   ; "Hacl_Poly1305_32"
   ; "Hacl_Poly1305_128"
+  ; "Hacl_Poly1305_256"
   ; "Hacl_NaCl"
   ; "EverCrypt_Error"
   ; "EverCrypt_CTR"
@@ -49,11 +51,15 @@ let modules =
   ; "Hacl_HPKE_Curve51_CP128_SHA512"
   ; "Hacl_GenericField32"
   ; "Hacl_Bignum256"
+  ; "Hacl_SHA2_Vec256"
   ; "Hacl_Bignum4096"
   ; "Hacl_Chacha20_Vec32"
   ; "EverCrypt_Ed25519"
   ; "Hacl_Bignum4096_32"
   ; "Hacl_HPKE_P256_CP128_SHA256"
+  ; "Hacl_Chacha20_Vec256"
+  ; "Hacl_Chacha20Poly1305_256"
+  ; "Hacl_HPKE_Curve51_CP256_SHA512"
   ; "Hacl_SHA2_Scalar32"
   ; "Hacl_Frodo976"
   ; "Hacl_HMAC_Blake2s_128"
@@ -68,12 +74,16 @@ let modules =
   ; "Hacl_HPKE_Curve51_CP32_SHA256"
   ; "Hacl_Streaming_Poly1305_32"
   ; "Hacl_HPKE_Curve51_CP32_SHA512"
+  ; "Hacl_HPKE_P256_CP256_SHA256"
   ; "Hacl_HPKE_P256_CP32_SHA256"
   ; "Hacl_Bignum64"
   ; "Hacl_Frodo64"
   ; "Hacl_Streaming_SHA1"
   ; "Hacl_Streaming_MD5"
+  ; "Hacl_HMAC_Blake2b_256"
+  ; "Hacl_HKDF_Blake2b_256"
   ; "Hacl_EC_Ed25519"
+  ; "Hacl_HPKE_Curve51_CP256_SHA256"
   ; "EverCrypt_Chacha20Poly1305"
   ; "EverCrypt_AEAD"
   ; "EverCrypt_HMAC"

diff --git a/hacl-star-raw.opam b/hacl-star-raw.opam
@@ -23,6 +23,7 @@ depends: [
 available: [
   arch != "ppc64" & arch != "ppc32" &
   arch != "arm32" & arch != "x86_32" &
+  arch != "arm64" & arch != "s390x" &
   (os = "freebsd" | os-family != "bsd")
 ]
 x-ci-accept-failures: [

diff --git a/raw/configure b/raw/configure
@@ -458,8 +458,15 @@ if detect_powerpc; then
   fi
 fi
 
-# dune port: disable some arch-specific code
-compile_vec256=false
+# dune port: require vec128 and vec256, disable detection for vale
+if ! $compile_vec128; then
+  echo "$CC $CROSS_CFLAGS cannot compile 128-bit vector arithmetic, disabling"
+  exit 1
+fi
+if ! $compile_vec256; then
+  echo "$build_target does not support 256-bit arithmetic"
+  exit 1
+fi
 compile_vale=false
 
 if $compile_intrinsics; then