Proper HACL* revision

python · gpshead · Feb 14, 2023 · Feb 8, 2023 · Feb 8, 2023 · Feb 14, 2023
commit 051e0a47742cb1ebe6952fb7248ba98290209382
@@ -250,18 +250,18 @@ static inline void sha224_finish(uint32_t *st, uint8_t *h)
   memcpy(h, hbuf, (uint32_t)28U * sizeof (uint8_t));
 }
 
-static inline void sha384_init(uint64_t *hash)
+void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash)
 {
   KRML_MAYBE_FOR8(i,
     (uint32_t)0U,
     (uint32_t)8U,
     (uint32_t)1U,
     uint64_t *os = hash;
-    uint64_t x = Hacl_Impl_SHA2_Generic_h384[i];
+    uint64_t x = Hacl_Impl_SHA2_Generic_h512[i];
     os[i] = x;);
 }
 
-static inline void sha384_update(uint8_t *b, uint64_t *hash)
+static inline void sha512_update(uint8_t *b, uint64_t *hash)
 {
   uint64_t hash_old[8U] = { 0U };
   uint64_t ws[16U] = { 0U };
@@ -381,19 +381,19 @@ static inline void sha384_update(uint8_t *b, uint64_t *hash)
     os[i] = x;);
 }
 
-static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
+static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
 {
   uint32_t blocks = len / (uint32_t)128U;
   for (uint32_t i = (uint32_t)0U; i < blocks; i++)
   {
     uint8_t *b0 = b;
     uint8_t *mb = b0 + i * (uint32_t)128U;
-    sha384_update(mb, st);
+    sha512_update(mb, st);
   }
 }
 
 static inline void
-sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash)
+sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash)
 {
   uint32_t blocks;
   if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U)
@@ -421,213 +421,56 @@ sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint6
   uint8_t *lb1 = l1;
   uint8_t *last0 = lb0;
   uint8_t *last1 = lb1;
-  sha384_update(last0, hash);
+  sha512_update(last0, hash);
   if (blocks > (uint32_t)1U)
   {
-    sha384_update(last1, hash);
+    sha512_update(last1, hash);
     return;
   }
 }
 
-static inline void sha384_finish(uint64_t *st, uint8_t *h)
+static inline void sha512_finish(uint64_t *st, uint8_t *h)
 {
   uint8_t hbuf[64U] = { 0U };
   KRML_MAYBE_FOR8(i,
     (uint32_t)0U,
     (uint32_t)8U,
     (uint32_t)1U,
     store64_be(hbuf + i * (uint32_t)8U, st[i]););
-  memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t));
+  memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t));
 }
 
-void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash)
+static inline void sha384_init(uint64_t *hash)
 {
   KRML_MAYBE_FOR8(i,
     (uint32_t)0U,
     (uint32_t)8U,
     (uint32_t)1U,
     uint64_t *os = hash;
-    uint64_t x = Hacl_Impl_SHA2_Generic_h512[i];
-    os[i] = x;);
-}
-
-static inline void sha512_update(uint8_t *b, uint64_t *hash)
-{
-  uint64_t hash_old[8U] = { 0U };
-  uint64_t ws[16U] = { 0U };
-  memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint64_t));
-  uint8_t *b10 = b;
-  uint64_t u = load64_be(b10);
-  ws[0U] = u;
-  uint64_t u0 = load64_be(b10 + (uint32_t)8U);
-  ws[1U] = u0;
-  uint64_t u1 = load64_be(b10 + (uint32_t)16U);
-  ws[2U] = u1;
-  uint64_t u2 = load64_be(b10 + (uint32_t)24U);
-  ws[3U] = u2;
-  uint64_t u3 = load64_be(b10 + (uint32_t)32U);
-  ws[4U] = u3;
-  uint64_t u4 = load64_be(b10 + (uint32_t)40U);
-  ws[5U] = u4;
-  uint64_t u5 = load64_be(b10 + (uint32_t)48U);
-  ws[6U] = u5;
-  uint64_t u6 = load64_be(b10 + (uint32_t)56U);
-  ws[7U] = u6;
-  uint64_t u7 = load64_be(b10 + (uint32_t)64U);
-  ws[8U] = u7;
-  uint64_t u8 = load64_be(b10 + (uint32_t)72U);
-  ws[9U] = u8;
-  uint64_t u9 = load64_be(b10 + (uint32_t)80U);
-  ws[10U] = u9;
-  uint64_t u10 = load64_be(b10 + (uint32_t)88U);
-  ws[11U] = u10;
-  uint64_t u11 = load64_be(b10 + (uint32_t)96U);
-  ws[12U] = u11;
-  uint64_t u12 = load64_be(b10 + (uint32_t)104U);
-  ws[13U] = u12;
-  uint64_t u13 = load64_be(b10 + (uint32_t)112U);
-  ws[14U] = u13;
-  uint64_t u14 = load64_be(b10 + (uint32_t)120U);
-  ws[15U] = u14;
-  KRML_MAYBE_FOR5(i0,
-    (uint32_t)0U,
-    (uint32_t)5U,
-    (uint32_t)1U,
-    KRML_MAYBE_FOR16(i,
-      (uint32_t)0U,
-      (uint32_t)16U,
-      (uint32_t)1U,
-      uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512[(uint32_t)16U * i0 + i];
-      uint64_t ws_t = ws[i];
-      uint64_t a0 = hash[0U];
-      uint64_t b0 = hash[1U];
-      uint64_t c0 = hash[2U];
-      uint64_t d0 = hash[3U];
-      uint64_t e0 = hash[4U];
-      uint64_t f0 = hash[5U];
-      uint64_t g0 = hash[6U];
-      uint64_t h02 = hash[7U];
-      uint64_t k_e_t = k_t;
-      uint64_t
-      t1 =
-        h02
-        +
-          ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U)
-          ^
-            ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U)
-            ^ (e0 << (uint32_t)23U | e0 >> (uint32_t)41U)))
-        + ((e0 & f0) ^ (~e0 & g0))
-        + k_e_t
-        + ws_t;
-      uint64_t
-      t2 =
-        ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U)
-        ^
-          ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U)
-          ^ (a0 << (uint32_t)25U | a0 >> (uint32_t)39U)))
-        + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0)));
-      uint64_t a1 = t1 + t2;
-      uint64_t b1 = a0;
-      uint64_t c1 = b0;
-      uint64_t d1 = c0;
-      uint64_t e1 = d0 + t1;
-      uint64_t f1 = e0;
-      uint64_t g1 = f0;
-      uint64_t h12 = g0;
-      hash[0U] = a1;
-      hash[1U] = b1;
-      hash[2U] = c1;
-      hash[3U] = d1;
-      hash[4U] = e1;
-      hash[5U] = f1;
-      hash[6U] = g1;
-      hash[7U] = h12;);
-    if (i0 < (uint32_t)4U)
-    {
-      KRML_MAYBE_FOR16(i,
-        (uint32_t)0U,
-        (uint32_t)16U,
-        (uint32_t)1U,
-        uint64_t t16 = ws[i];
-        uint64_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U];
-        uint64_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U];
-        uint64_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U];
-        uint64_t
-        s1 =
-          (t2 << (uint32_t)45U | t2 >> (uint32_t)19U)
-          ^ ((t2 << (uint32_t)3U | t2 >> (uint32_t)61U) ^ t2 >> (uint32_t)6U);
-        uint64_t
-        s0 =
-          (t15 << (uint32_t)63U | t15 >> (uint32_t)1U)
-          ^ ((t15 << (uint32_t)56U | t15 >> (uint32_t)8U) ^ t15 >> (uint32_t)7U);
-        ws[i] = s1 + t7 + s0 + t16;);
-    });
-  KRML_MAYBE_FOR8(i,
-    (uint32_t)0U,
-    (uint32_t)8U,
-    (uint32_t)1U,
-    uint64_t *os = hash;
-    uint64_t x = hash[i] + hash_old[i];
+    uint64_t x = Hacl_Impl_SHA2_Generic_h384[i];
     os[i] = x;);
 }
 
-static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
+static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
 {
-  uint32_t blocks = len / (uint32_t)128U;
-  for (uint32_t i = (uint32_t)0U; i < blocks; i++)
-  {
-    uint8_t *b0 = b;
-    uint8_t *mb = b0 + i * (uint32_t)128U;
-    sha512_update(mb, st);
-  }
+  sha512_update_nblocks(len, b, st);
 }
 
-static inline void
-sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash)
+static void
+sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st)
 {
-  uint32_t blocks;
-  if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U)
-  {
-    blocks = (uint32_t)1U;
-  }
-  else
-  {
-    blocks = (uint32_t)2U;
-  }
-  uint32_t fin = blocks * (uint32_t)128U;
-  uint8_t last[256U] = { 0U };
-  uint8_t totlen_buf[16U] = { 0U };
-  FStar_UInt128_uint128 total_len_bits = FStar_UInt128_shift_left(totlen, (uint32_t)3U);
-  store128_be(totlen_buf, total_len_bits);
-  uint8_t *b0 = b;
-  memcpy(last, b0, len * sizeof (uint8_t));
-  last[len] = (uint8_t)0x80U;
-  memcpy(last + fin - (uint32_t)16U, totlen_buf, (uint32_t)16U * sizeof (uint8_t));
-  uint8_t *last00 = last;
-  uint8_t *last10 = last + (uint32_t)128U;
-  uint8_t *l0 = last00;
-  uint8_t *l1 = last10;
-  uint8_t *lb0 = l0;
-  uint8_t *lb1 = l1;
-  uint8_t *last0 = lb0;
-  uint8_t *last1 = lb1;
-  sha512_update(last0, hash);
-  if (blocks > (uint32_t)1U)
-  {
-    sha512_update(last1, hash);
-    return;
-  }
+  sha512_update_last(totlen, len, b, st);
 }
 
-static inline void sha512_finish(uint64_t *st, uint8_t *h)
+static inline void sha384_finish(uint64_t *st, uint8_t *h)
 {
   uint8_t hbuf[64U] = { 0U };
   KRML_MAYBE_FOR8(i,
     (uint32_t)0U,
     (uint32_t)8U,
     (uint32_t)1U,
     store64_be(hbuf + i * (uint32_t)8U, st[i]););
-  memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t));
+  memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t));
 }
 
 /**
@@ -1076,6 +919,34 @@ Hacl_Streaming_SHA2_state_sha2_384 *Hacl_Streaming_SHA2_create_in_512(void)
   return p;
 }
 
+/**
+Copies the state passed as argument into a newly allocated state (deep copy).
+The state is to be freed by calling `free_512`. Cloning the state this way is
+useful, for instance, if your control-flow diverges and you need to feed
+more (different) data into the hash in each branch.
+*/
+Hacl_Streaming_SHA2_state_sha2_384
+*Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_SHA2_state_sha2_384 *s0)
+{
+  Hacl_Streaming_SHA2_state_sha2_384 scrut = *s0;
+  uint64_t *block_state0 = scrut.block_state;
+  uint8_t *buf0 = scrut.buf;
+  uint64_t total_len0 = scrut.total_len;
+  uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t));
+  memcpy(buf, buf0, (uint32_t)128U * sizeof (uint8_t));
+  uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t));
+  memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint64_t));
+  Hacl_Streaming_SHA2_state_sha2_384
+  s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
+  Hacl_Streaming_SHA2_state_sha2_384
+  *p =
+    (Hacl_Streaming_SHA2_state_sha2_384 *)KRML_HOST_MALLOC(sizeof (
+        Hacl_Streaming_SHA2_state_sha2_384
+      ));
+  p[0U] = s;
+  return p;
+}
+
 void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_SHA2_state_sha2_384 *s)
 {
   Hacl_Streaming_SHA2_state_sha2_384 scrut = *s;

@@ -38,7 +38,6 @@ extern "C" {
 
 
 
-
 typedef struct Hacl_Streaming_SHA2_state_sha2_224_s
 {
   uint32_t *block_state;
@@ -140,6 +139,15 @@ void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst
 
 Hacl_Streaming_SHA2_state_sha2_384 *Hacl_Streaming_SHA2_create_in_512(void);
 
+/**
+Copies the state passed as argument into a newly allocated state (deep copy).
+The state is to be freed by calling `free_512`. Cloning the state this way is
+useful, for instance, if your control-flow diverges and you need to feed
+more (different) data into the hash in each branch.
+*/
+Hacl_Streaming_SHA2_state_sha2_384
+*Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_SHA2_state_sha2_384 *s0);
+
 void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_SHA2_state_sha2_384 *s);
 
 /**

@@ -7,12 +7,13 @@
 #ifndef __FStar_UInt128_Verified_H
 #define __FStar_UInt128_Verified_H
 
+
+
 #include "FStar_UInt_8_16_32_64.h"
 #include <inttypes.h>
 #include <stdbool.h>
 #include "krml/types.h"
 #include "krml/internal/target.h"
-
 static inline uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
 {
   return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U;

@@ -7,13 +7,15 @@
 #ifndef __FStar_UInt_8_16_32_64_H
 #define __FStar_UInt_8_16_32_64_H
 
+
+
+
 #include <inttypes.h>
 #include <stdbool.h>
 
 #include "krml/lowstar_endianness.h"
 #include "krml/types.h"
 #include "krml/internal/target.h"
-
 static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
 {
   uint64_t x = a ^ b;

diff --git a/Modules/_hacl/include/krml/internal/target.h b/Modules/_hacl/include/krml/internal/target.h
@@ -31,10 +31,6 @@
 #  define KRML_HOST_FREE free
 #endif
 
-#ifndef KRML_HOST_IGNORE
-#  define KRML_HOST_IGNORE(x) (void)(x)
-#endif
-
 /* Macros for prettier unrolling of loops */
 #define KRML_LOOP1(i, n, x) { \
   x \

@@ -35,9 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-
-
-
 static const
 uint32_t
 Hacl_Impl_SHA2_Generic_h224[8U] =

@@ -22,7 +22,7 @@ fi
 
 # Update this when updating to a new version after verifying that the changes
 # the update brings in are good.
-expected_hacl_star_rev=99bf1eb0141e4d7325d333aac671a063dbc5f8c5
+expected_hacl_star_rev=4751fc2b11639f651718abf8522fcc36902ca67c
 
 hacl_dir="$(realpath "$1")"
 cd "$(dirname "$0")"