[CI] update code

cryspen · Nov 9, 2023 · 83ff172 · 83ff172
1 parent 4d3ac1c
commit 83ff172
Show file tree

Hide file tree

Showing 193 changed files with 37,749 additions and 44,341 deletions.
diff --git a/include/EverCrypt_Hash.h b/include/EverCrypt_Hash.h
@@ -121,29 +121,29 @@ EverCrypt_Hash_Incremental_hash(
   uint32_t len
 );
 
-#define MD5_HASH_LEN ((uint32_t)16U)
+#define MD5_HASH_LEN (16U)
 
-#define SHA1_HASH_LEN ((uint32_t)20U)
+#define SHA1_HASH_LEN (20U)
 
-#define SHA2_224_HASH_LEN ((uint32_t)28U)
+#define SHA2_224_HASH_LEN (28U)
 
-#define SHA2_256_HASH_LEN ((uint32_t)32U)
+#define SHA2_256_HASH_LEN (32U)
 
-#define SHA2_384_HASH_LEN ((uint32_t)48U)
+#define SHA2_384_HASH_LEN (48U)
 
-#define SHA2_512_HASH_LEN ((uint32_t)64U)
+#define SHA2_512_HASH_LEN (64U)
 
-#define SHA3_224_HASH_LEN ((uint32_t)28U)
+#define SHA3_224_HASH_LEN (28U)
 
-#define SHA3_256_HASH_LEN ((uint32_t)32U)
+#define SHA3_256_HASH_LEN (32U)
 
-#define SHA3_384_HASH_LEN ((uint32_t)48U)
+#define SHA3_384_HASH_LEN (48U)
 
-#define SHA3_512_HASH_LEN ((uint32_t)64U)
+#define SHA3_512_HASH_LEN (64U)
 
-#define BLAKE2S_HASH_LEN ((uint32_t)32U)
+#define BLAKE2S_HASH_LEN (32U)
 
-#define BLAKE2B_HASH_LEN ((uint32_t)64U)
+#define BLAKE2B_HASH_LEN (64U)
 
 #if defined(__cplusplus)
 }

diff --git a/include/Hacl_IntTypes_Intrinsics.h b/include/Hacl_IntTypes_Intrinsics.h
@@ -41,7 +41,7 @@ static inline uint32_t
 Hacl_IntTypes_Intrinsics_add_carry_u32(uint32_t cin, uint32_t x, uint32_t y, uint32_t *r)
 {
   uint64_t res = (uint64_t)x + (uint64_t)cin + (uint64_t)y;
-  uint32_t c = (uint32_t)(res >> (uint32_t)32U);
+  uint32_t c = (uint32_t)(res >> 32U);
   r[0U] = (uint32_t)res;
   return c;
 }
@@ -50,7 +50,7 @@ static inline uint32_t
 Hacl_IntTypes_Intrinsics_sub_borrow_u32(uint32_t cin, uint32_t x, uint32_t y, uint32_t *r)
 {
   uint64_t res = (uint64_t)x - (uint64_t)y - (uint64_t)cin;
-  uint32_t c = (uint32_t)(res >> (uint32_t)32U) & (uint32_t)1U;
+  uint32_t c = (uint32_t)(res >> 32U) & 1U;
   r[0U] = (uint32_t)res;
   return c;
 }
@@ -59,8 +59,7 @@ static inline uint64_t
 Hacl_IntTypes_Intrinsics_add_carry_u64(uint64_t cin, uint64_t x, uint64_t y, uint64_t *r)
 {
   uint64_t res = x + cin + y;
-  uint64_t
-  c = (~FStar_UInt64_gte_mask(res, x) | (FStar_UInt64_eq_mask(res, x) & cin)) & (uint64_t)1U;
+  uint64_t c = (~FStar_UInt64_gte_mask(res, x) | (FStar_UInt64_eq_mask(res, x) & cin)) & 1ULL;
   r[0U] = res;
   return c;
 }
@@ -73,7 +72,7 @@ Hacl_IntTypes_Intrinsics_sub_borrow_u64(uint64_t cin, uint64_t x, uint64_t y, ui
   c =
     ((FStar_UInt64_gte_mask(res, x) & ~FStar_UInt64_eq_mask(res, x))
     | (FStar_UInt64_eq_mask(res, x) & cin))
-    & (uint64_t)1U;
+    & 1ULL;
   r[0U] = res;
   return c;
 }

diff --git a/include/Hacl_IntTypes_Intrinsics_128.h b/include/Hacl_IntTypes_Intrinsics_128.h
@@ -45,7 +45,7 @@ Hacl_IntTypes_Intrinsics_128_add_carry_u64(uint64_t cin, uint64_t x, uint64_t y,
     FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_uint64_to_uint128(x),
         FStar_UInt128_uint64_to_uint128(cin)),
       FStar_UInt128_uint64_to_uint128(y));
-  uint64_t c = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, (uint32_t)64U));
+  uint64_t c = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, 64U));
   r[0U] = FStar_UInt128_uint128_to_uint64(res);
   return c;
 }
@@ -58,10 +58,7 @@ Hacl_IntTypes_Intrinsics_128_sub_borrow_u64(uint64_t cin, uint64_t x, uint64_t y
     FStar_UInt128_sub_mod(FStar_UInt128_sub_mod(FStar_UInt128_uint64_to_uint128(x),
         FStar_UInt128_uint64_to_uint128(y)),
       FStar_UInt128_uint64_to_uint128(cin));
-  uint64_t
-  c =
-    FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, (uint32_t)64U))
-    & (uint64_t)1U;
+  uint64_t c = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, 64U)) & 1ULL;
   r[0U] = FStar_UInt128_uint128_to_uint64(res);
   return c;
 }

diff --git a/include/internal/Hacl_Bignum25519_51.h b/include/internal/Hacl_Bignum25519_51.h