Merge 59f7ba5 into 4d3ac1c

cryspen · Nov 21, 2023 · 8028e68 · 8028e68
2 parents 4d3ac1c + 59f7ba5
commit 8028e68
Show file tree

Hide file tree

Showing 210 changed files with 37,702 additions and 45,318 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_Bignum.h b/include/internal/Hacl_Bignum.h
@@ -124,15 +124,6 @@ Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u32(
   uint32_t *res
 );
 
-void
-Hacl_Bignum_Montgomery_bn_mont_reduction_u32(
-  uint32_t len,
-  uint32_t *n,
-  uint32_t nInv,
-  uint32_t *c,
-  uint32_t *res
-);
-
 void
 Hacl_Bignum_Montgomery_bn_to_mont_u32(
   uint32_t len,
@@ -181,15 +172,6 @@ Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u64(
   uint64_t *res
 );
 
-void
-Hacl_Bignum_Montgomery_bn_mont_reduction_u64(
-  uint32_t len,
-  uint64_t *n,
-  uint64_t nInv,
-  uint64_t *c,
-  uint64_t *res
-);
-
 void
 Hacl_Bignum_Montgomery_bn_to_mont_u64(
   uint32_t len,
@@ -228,6 +210,24 @@ Hacl_Bignum_Montgomery_bn_mont_sqr_u64(
   uint64_t *resM
 );
 
+void
+Hacl_Bignum_AlmostMontgomery_bn_almost_mont_reduction_u32(
+  uint32_t len,
+  uint32_t *n,
+  uint32_t nInv,
+  uint32_t *c,
+  uint32_t *res
+);
+
+void
+Hacl_Bignum_AlmostMontgomery_bn_almost_mont_reduction_u64(
+  uint32_t len,
+  uint64_t *n,
+  uint64_t nInv,
+  uint64_t *c,
+  uint64_t *res
+);
+
 uint32_t
 Hacl_Bignum_Exponentiation_bn_check_mod_exp_u32(
   uint32_t len,