[CI] update code

cryspen · Mar 16, 2024 · bd061ec · bd061ec
1 parent b999846
commit bd061ec
Show file tree

Hide file tree

Showing 29 changed files with 598 additions and 54 deletions.
diff --git a/include/internal/Hacl_Hash_Blake2b.h b/include/internal/Hacl_Hash_Blake2b.h
@@ -38,6 +38,38 @@ extern "C" {
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "../Hacl_Hash_Blake2b.h"
 
+typedef struct Hacl_Hash_Blake2s_blake2s_params_s
+{
+  uint8_t digest_length;
+  uint8_t key_length;
+  uint8_t fanout;
+  uint8_t depth;
+  uint32_t leaf_length;
+  uint32_t node_offset;
+  uint16_t xof_length;
+  uint8_t node_depth;
+  uint8_t inner_length;
+  uint8_t *salt;
+  uint8_t *personal;
+}
+Hacl_Hash_Blake2s_blake2s_params;
+
+typedef struct Hacl_Hash_Blake2s_blake2b_params_s
+{
+  uint8_t digest_length1;
+  uint8_t key_length1;
+  uint8_t fanout1;
+  uint8_t depth1;
+  uint32_t leaf_length1;
+  uint32_t node_offset1;
+  uint32_t xof_length1;
+  uint8_t node_depth1;
+  uint8_t inner_length1;
+  uint8_t *salt1;
+  uint8_t *personal1;
+}
+Hacl_Hash_Blake2s_blake2b_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
@@ -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
@@ -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
@@ -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/internal/Hacl_Hash_Blake2b.h b/include/msvc/internal/Hacl_Hash_Blake2b.h
@@ -38,6 +38,38 @@ extern "C" {
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "../Hacl_Hash_Blake2b.h"
 
+typedef struct Hacl_Hash_Blake2s_blake2s_params_s
+{
+  uint8_t digest_length;
+  uint8_t key_length;
+  uint8_t fanout;
+  uint8_t depth;
+  uint32_t leaf_length;
+  uint32_t node_offset;
+  uint16_t xof_length;
+  uint8_t node_depth;
+  uint8_t inner_length;
+  uint8_t *salt;
+  uint8_t *personal;
+}
+Hacl_Hash_Blake2s_blake2s_params;
+
+typedef struct Hacl_Hash_Blake2s_blake2b_params_s
+{
+  uint8_t digest_length1;
+  uint8_t key_length1;
+  uint8_t fanout1;
+  uint8_t depth1;
+  uint32_t leaf_length1;
+  uint32_t node_offset1;
+  uint32_t xof_length1;
+  uint8_t node_depth1;
+  uint8_t inner_length1;
+  uint8_t *salt1;
+  uint8_t *personal1;
+}
+Hacl_Hash_Blake2s_blake2b_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
@@ -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
@@ -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
@@ -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/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml b/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml
@@ -5,6 +5,62 @@ 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_blake2s_params =
+      [ `hacl_Hash_Blake2s_blake2s_params ] structure
+    let (hacl_Hash_Blake2s_blake2s_params :
+      [ `hacl_Hash_Blake2s_blake2s_params ] structure typ) =
+      structure "Hacl_Hash_Blake2s_blake2s_params_s"
+    let hacl_Hash_Blake2s_blake2s_params_digest_length =
+      field hacl_Hash_Blake2s_blake2s_params "digest_length" uint8_t
+    let hacl_Hash_Blake2s_blake2s_params_key_length =
+      field hacl_Hash_Blake2s_blake2s_params "key_length" uint8_t
+    let hacl_Hash_Blake2s_blake2s_params_fanout =
+      field hacl_Hash_Blake2s_blake2s_params "fanout" uint8_t
+    let hacl_Hash_Blake2s_blake2s_params_depth =
+      field hacl_Hash_Blake2s_blake2s_params "depth" uint8_t
+    let hacl_Hash_Blake2s_blake2s_params_leaf_length =
+      field hacl_Hash_Blake2s_blake2s_params "leaf_length" uint32_t
+    let hacl_Hash_Blake2s_blake2s_params_node_offset =
+      field hacl_Hash_Blake2s_blake2s_params "node_offset" uint32_t
+    let hacl_Hash_Blake2s_blake2s_params_xof_length =
+      field hacl_Hash_Blake2s_blake2s_params "xof_length" uint16_t
+    let hacl_Hash_Blake2s_blake2s_params_node_depth =
+      field hacl_Hash_Blake2s_blake2s_params "node_depth" uint8_t
+    let hacl_Hash_Blake2s_blake2s_params_inner_length =
+      field hacl_Hash_Blake2s_blake2s_params "inner_length" uint8_t
+    let hacl_Hash_Blake2s_blake2s_params_salt =
+      field hacl_Hash_Blake2s_blake2s_params "salt" (ptr uint8_t)
+    let hacl_Hash_Blake2s_blake2s_params_personal =
+      field hacl_Hash_Blake2s_blake2s_params "personal" (ptr uint8_t)
+    let _ = seal hacl_Hash_Blake2s_blake2s_params
+    type hacl_Hash_Blake2s_blake2b_params =
+      [ `hacl_Hash_Blake2s_blake2b_params ] structure
+    let (hacl_Hash_Blake2s_blake2b_params :
+      [ `hacl_Hash_Blake2s_blake2b_params ] structure typ) =
+      structure "Hacl_Hash_Blake2s_blake2b_params_s"
+    let hacl_Hash_Blake2s_blake2b_params_digest_length1 =
+      field hacl_Hash_Blake2s_blake2b_params "digest_length1" uint8_t
+    let hacl_Hash_Blake2s_blake2b_params_key_length1 =
+      field hacl_Hash_Blake2s_blake2b_params "key_length1" uint8_t
+    let hacl_Hash_Blake2s_blake2b_params_fanout1 =
+      field hacl_Hash_Blake2s_blake2b_params "fanout1" uint8_t
+    let hacl_Hash_Blake2s_blake2b_params_depth1 =
+      field hacl_Hash_Blake2s_blake2b_params "depth1" uint8_t
+    let hacl_Hash_Blake2s_blake2b_params_leaf_length1 =
+      field hacl_Hash_Blake2s_blake2b_params "leaf_length1" uint32_t
+    let hacl_Hash_Blake2s_blake2b_params_node_offset1 =
+      field hacl_Hash_Blake2s_blake2b_params "node_offset1" uint32_t
+    let hacl_Hash_Blake2s_blake2b_params_xof_length1 =
+      field hacl_Hash_Blake2s_blake2b_params "xof_length1" uint32_t
+    let hacl_Hash_Blake2s_blake2b_params_node_depth1 =
+      field hacl_Hash_Blake2s_blake2b_params "node_depth1" uint8_t
+    let hacl_Hash_Blake2s_blake2b_params_inner_length1 =
+      field hacl_Hash_Blake2s_blake2b_params "inner_length1" uint8_t
+    let hacl_Hash_Blake2s_blake2b_params_salt1 =
+      field hacl_Hash_Blake2s_blake2b_params "salt1" (ptr uint8_t)
+    let hacl_Hash_Blake2s_blake2b_params_personal1 =
+      field hacl_Hash_Blake2s_blake2b_params "personal1" (ptr uint8_t)
+    let _ = seal hacl_Hash_Blake2s_blake2b_params
     let hacl_Hash_Blake2b_init =
       foreign "Hacl_Hash_Blake2b_init"
         ((ptr uint64_t) @-> (uint32_t @-> (uint32_t @-> (returning void))))

diff --git 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,68 @@ 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_blake2b_params
+  p =
+    {
+      .digest_length1 = 64U, .key_length1 = 0U, .fanout1 = 1U, .depth1 = 1U, .leaf_length1 = 0U,
+      .node_offset1 = 0U, .xof_length1 = 0U, .node_depth1 = 0U, .inner_length1 = 0U, .salt1 = salt,
+      .personal1 = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 4U;
+    uint8_t *bj = p.salt1 + 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.personal1 + 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.fanout1 << 16U ^ ((uint64_t)p.depth1 << 24U ^ (uint64_t)p.leaf_length1 << 32U)));
+  tmp[1U] = (uint64_t)p.node_offset1 ^ (uint64_t)p.xof_length1 << 32U;
+  tmp[2U] = (uint64_t)p.node_depth1 ^ (uint64_t)p.inner_length1 << 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)

diff --git 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,62 @@ 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_blake2b_params
+  p =
+    {
+      .digest_length1 = 64U, .key_length1 = 0U, .fanout1 = 1U, .depth1 = 1U, .leaf_length1 = 0U,
+      .node_offset1 = 0U, .xof_length1 = 0U, .node_depth1 = 0U, .inner_length1 = 0U, .salt1 = salt,
+      .personal1 = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 4U;
+    uint8_t *bj = p.salt1 + 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.personal1 + 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.fanout1 << 16U ^ ((uint64_t)p.depth1 << 24U ^ (uint64_t)p.leaf_length1 << 32U)));
+  tmp[1U] = (uint64_t)p.node_offset1 ^ (uint64_t)p.xof_length1 << 32U;
+  tmp[2U] = (uint64_t)p.node_depth1 ^ (uint64_t)p.inner_length1 << 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