Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

update to hacl 309736b87a124ad1bdc2dc34e7768568039639e5 #430

Closed
wants to merge 4 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions include/EverCrypt_Hash.h
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Expand Down
9 changes: 4 additions & 5 deletions include/Hacl_IntTypes_Intrinsics.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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;
}
Expand All @@ -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;
}
Expand All @@ -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;
}
Expand Down
7 changes: 2 additions & 5 deletions include/Hacl_IntTypes_Intrinsics_128.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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;
}
Expand Down
36 changes: 18 additions & 18 deletions include/internal/Hacl_Bignum.h
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down
Loading
Loading