Merge pull request hacl-star#822 from hacl-star/protz_hints_and_dist

Hints & dist

dist/gcc-compatible/INFO.txt

@@ -1,4 +1,4 @@
 This code was generated with the following toolchain.
-F* version: 5a6ace4987b2e4a9a4395cc95411c4f4b9dbd44a
-KaRaMeL version: 46454baace30ebd4c79c8f1f3c91056875bf346f
+F* version: 504c21f3c02a82d5ed2d2db746245157c995e9e5
+KaRaMeL version: 2cf2974007f4103dba5619e4eb9e3eaeefad533b
 Vale version: 0.3.19

dist/mozilla/Hacl_Hash_SHA1.c

@@ -263,14 +263,14 @@ void Hacl_Streaming_SHA1_legacy_init(Hacl_Streaming_MD_state_32 *s)
 /**
 0 = success, 1 = max length exceeded
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA1_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_MD_state_32 s = *p;
   uint64_t total_len = s.total_len;
   if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -435,7 +435,7 @@ Hacl_Streaming_SHA1_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data,
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 void Hacl_Streaming_SHA1_legacy_finish(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)

dist/mozilla/Hacl_Hash_SHA1.h

@@ -46,7 +46,7 @@ void Hacl_Streaming_SHA1_legacy_init(Hacl_Streaming_MD_state_32 *s);
 /**
 0 = success, 1 = max length exceeded
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA1_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len);
 
 void Hacl_Streaming_SHA1_legacy_finish(Hacl_Streaming_MD_state_32 *p, uint8_t *dst);

dist/mozilla/Hacl_Hash_SHA2.c

@@ -543,14 +543,14 @@ void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s)
   s[0U] = tmp;
 }
 
-static inline uint32_t
+static inline Hacl_Streaming_Types_error_code
 update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_MD_state_32 s = *p;
   uint64_t total_len = s.total_len;
   if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -719,7 +719,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 /**
@@ -729,7 +729,7 @@ success, or 1 if the combined length of all of the data passed to `update_256`
 
 This function is identical to the update function for SHA2_224.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_256(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -841,7 +841,7 @@ void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s)
   s[0U] = tmp;
 }
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_224(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -966,14 +966,14 @@ void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s)
   s[0U] = tmp;
 }
 
-static inline uint32_t
+static inline Hacl_Streaming_Types_error_code
 update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_MD_state_64 s = *p;
   uint64_t total_len = s.total_len;
   if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -1142,7 +1142,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 /**
@@ -1152,7 +1152,7 @@ success, or 1 if the combined length of all of the data passed to `update_512`
 
 This function is identical to the update function for SHA2_384.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_512(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,
@@ -1265,7 +1265,7 @@ void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s)
   s[0U] = tmp;
 }
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_384(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,

dist/mozilla/Hacl_Hash_SHA2.h

@@ -72,7 +72,7 @@ success, or 1 if the combined length of all of the data passed to `update_256`
 
 This function is identical to the update function for SHA2_224.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_256(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -103,7 +103,7 @@ Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void);
 
 void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s);
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_224(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -143,7 +143,7 @@ success, or 1 if the combined length of all of the data passed to `update_512`
 
 This function is identical to the update function for SHA2_384.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_512(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,
@@ -174,7 +174,7 @@ Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void);
 
 void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s);
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_384(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,

dist/mozilla/Hacl_Hash_SHA3.c

@@ -184,8 +184,7 @@ Hacl_Streaming_Keccak_state *Hacl_Streaming_Keccak_malloc(Spec_Hash_Definitions_
   *p = (Hacl_Streaming_Keccak_state *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_Keccak_state));
   p[0U] = s;
   uint64_t *s1 = block_state.snd;
-  for (uint32_t _i = 0U; _i < (uint32_t)25U; ++_i)
-    ((void **)s1)[_i] = (void *)(uint64_t)0U;
+  memset(s1, 0U, (uint32_t)25U * sizeof (uint64_t));
   return p;
 }
 
@@ -230,14 +229,13 @@ void Hacl_Streaming_Keccak_reset(Hacl_Streaming_Keccak_state *s)
   uint8_t *buf = scrut.buf;
   Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state;
   uint64_t *s1 = block_state.snd;
-  for (uint32_t _i = 0U; _i < (uint32_t)25U; ++_i)
-    ((void **)s1)[_i] = (void *)(uint64_t)0U;
+  memset(s1, 0U, (uint32_t)25U * sizeof (uint64_t));
   Hacl_Streaming_Keccak_state
   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
   s[0U] = tmp;
 }
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_Keccak_state s = *p;
@@ -246,7 +244,7 @@ Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint
   Spec_Hash_Definitions_hash_alg i = block_state.fst;
   if ((uint64_t)len > (uint64_t)0xFFFFFFFFFFFFFFFFU - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)block_len(i) == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -419,7 +417,7 @@ Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 static void
@@ -486,32 +484,32 @@ finish_(
   Hacl_Impl_SHA3_squeeze(s, block_len(a11), hash_len(a11), dst);
 }
 
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_finish(Hacl_Streaming_Keccak_state *s, uint8_t *dst)
 {
   Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
   if (a1 == Spec_Hash_Definitions_Shake128 || a1 == Spec_Hash_Definitions_Shake256)
   {
-    return Hacl_Streaming_Keccak_InvalidAlgorithm;
+    return Hacl_Streaming_Types_InvalidAlgorithm;
   }
   finish_(a1, s, dst, hash_len(a1));
-  return Hacl_Streaming_Keccak_Success;
+  return Hacl_Streaming_Types_Success;
 }
 
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_squeeze(Hacl_Streaming_Keccak_state *s, uint8_t *dst, uint32_t l)
 {
   Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
   if (!(a1 == Spec_Hash_Definitions_Shake128 || a1 == Spec_Hash_Definitions_Shake256))
   {
-    return Hacl_Streaming_Keccak_InvalidAlgorithm;
+    return Hacl_Streaming_Types_InvalidAlgorithm;
   }
   if (l == (uint32_t)0U)
   {
-    return Hacl_Streaming_Keccak_InvalidLength;
+    return Hacl_Streaming_Types_InvalidLength;
   }
   finish_(a1, s, dst, l);
-  return Hacl_Streaming_Keccak_Success;
+  return Hacl_Streaming_Types_Success;
 }
 
 uint32_t Hacl_Streaming_Keccak_block_len(Hacl_Streaming_Keccak_state *s)

dist/mozilla/Hacl_Hash_SHA3.h

@@ -62,19 +62,13 @@ Hacl_Streaming_Keccak_state *Hacl_Streaming_Keccak_copy(Hacl_Streaming_Keccak_st
 
 void Hacl_Streaming_Keccak_reset(Hacl_Streaming_Keccak_state *s);
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint32_t len);
 
-#define Hacl_Streaming_Keccak_Success 0
-#define Hacl_Streaming_Keccak_InvalidAlgorithm 1
-#define Hacl_Streaming_Keccak_InvalidLength 2
-
-typedef uint8_t Hacl_Streaming_Keccak_error_code;
-
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_finish(Hacl_Streaming_Keccak_state *s, uint8_t *dst);
 
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_squeeze(Hacl_Streaming_Keccak_state *s, uint8_t *dst, uint32_t l);
 
 uint32_t Hacl_Streaming_Keccak_block_len(Hacl_Streaming_Keccak_state *s);

dist/mozilla/Hacl_Streaming_Types.h

@@ -52,6 +52,13 @@ extern "C" {
 
 typedef uint8_t Spec_Hash_Definitions_hash_alg;
 
+#define Hacl_Streaming_Types_Success 0
+#define Hacl_Streaming_Types_InvalidAlgorithm 1
+#define Hacl_Streaming_Types_InvalidLength 2
+#define Hacl_Streaming_Types_MaximumLengthExceeded 3
+
+typedef uint8_t Hacl_Streaming_Types_error_code;
+
 typedef struct Hacl_Streaming_MD_state_32_s
 {
   uint32_t *block_state;

dist/mozilla/Makefile.include

@@ -2,4 +2,4 @@ USER_TARGET=libevercrypt.a
 USER_CFLAGS=-Wno-unused
 USER_C_FILES=Lib_Memzero0.c
 ALL_C_FILES=Hacl_Bignum.c Hacl_Chacha20.c Hacl_Chacha20Poly1305_128.c Hacl_Chacha20Poly1305_256.c Hacl_Chacha20Poly1305_32.c Hacl_Chacha20_Vec128.c Hacl_Chacha20_Vec256.c Hacl_Curve25519_51.c Hacl_Curve25519_64.c Hacl_Hash_SHA1.c Hacl_Hash_SHA2.c Hacl_Hash_SHA3.c Hacl_Poly1305_128.c Hacl_Poly1305_256.c Hacl_Poly1305_32.c Hacl_RSAPSS.c Lib_Memzero0.c Vale.c
-ALL_H_FILES=Hacl_Bignum.h Hacl_Chacha20.h Hacl_Chacha20Poly1305_128.h Hacl_Chacha20Poly1305_256.h Hacl_Chacha20Poly1305_32.h Hacl_Chacha20_Vec128.h Hacl_Chacha20_Vec256.h Hacl_Curve25519_51.h Hacl_Curve25519_64.h Hacl_Hash_SHA1.h Hacl_Hash_SHA2.h Hacl_Hash_SHA3.h Hacl_IntTypes_Intrinsics.h Hacl_IntTypes_Intrinsics_128.h Hacl_Krmllib.h Hacl_Poly1305_128.h Hacl_Poly1305_256.h Hacl_Poly1305_32.h Hacl_RSAPSS.h Hacl_Spec.h Hacl_Streaming_Types.h Lib_Memzero0.h TestLib.h curve25519-inline.h lib_intrinsics.h libintvector.h
+ALL_H_FILES=config.h curve25519-inline.h Hacl_Bignum.h Hacl_Chacha20.h Hacl_Chacha20Poly1305_128.h Hacl_Chacha20Poly1305_256.h Hacl_Chacha20Poly1305_32.h Hacl_Chacha20_Vec128.h Hacl_Chacha20_Vec256.h Hacl_Curve25519_51.h Hacl_Curve25519_64.h Hacl_Hash_SHA1.h Hacl_Hash_SHA2.h Hacl_Hash_SHA3.h Hacl_IntTypes_Intrinsics_128.h Hacl_IntTypes_Intrinsics.h Hacl_Krmllib.h Hacl_Poly1305_128.h Hacl_Poly1305_256.h Hacl_Poly1305_32.h Hacl_RSAPSS.h Hacl_Spec.h Hacl_Streaming_Types.h lib_intrinsics.h libintvector.h Lib_Memzero0.h TestLib.h