gh-99108: Refresh HACL*; update modules accordingly; fix namespacing (GH-117237)

Pulls in a new update from https://github.com/hacl-star/hacl-star and fixes our C "namespacing" done by `Modules/_hacl/refresh.sh`.
This commit is contained in:
Jonathan Protzenko 2024-03-25 17:35:26 -07:00 committed by GitHub
parent 8945b7ff55
commit 872e212378
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
23 changed files with 1603 additions and 1843 deletions

View file

@ -15,7 +15,7 @@
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;
return (a ^ ((a ^ b) | ((a - b) ^ b))) >> 63U;
}
static inline uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b)
@ -118,7 +118,7 @@ static inline FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a
return lit;
}
static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
static uint32_t FStar_UInt128_u32_64 = 64U;
static inline uint64_t FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s)
{
@ -134,7 +134,7 @@ FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s)
static inline FStar_UInt128_uint128
FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t)0U)
if (s == 0U)
{
return a;
}
@ -151,7 +151,7 @@ static inline FStar_UInt128_uint128
FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)
{
FStar_UInt128_uint128 lit;
lit.low = (uint64_t)0U;
lit.low = 0ULL;
lit.high = a.low << (s - FStar_UInt128_u32_64);
return lit;
}
@ -183,7 +183,7 @@ FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s)
static inline FStar_UInt128_uint128
FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)
{
if (s == (uint32_t)0U)
if (s == 0U)
{
return a;
}
@ -201,7 +201,7 @@ FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)
{
FStar_UInt128_uint128 lit;
lit.low = a.high >> (s - FStar_UInt128_u32_64);
lit.high = (uint64_t)0U;
lit.high = 0ULL;
return lit;
}
@ -269,7 +269,7 @@ static inline FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a)
{
FStar_UInt128_uint128 lit;
lit.low = a;
lit.high = (uint64_t)0U;
lit.high = 0ULL;
return lit;
}
@ -280,10 +280,10 @@ static inline uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)
static inline uint64_t FStar_UInt128_u64_mod_32(uint64_t a)
{
return a & (uint64_t)0xffffffffU;
return a & 0xffffffffULL;
}
static uint32_t FStar_UInt128_u32_32 = (uint32_t)32U;
static uint32_t FStar_UInt128_u32_32 = 32U;
static inline uint64_t FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo)
{