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.

Sign up for GitHub

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 HACL to 1b30697fc2b0d8d5e2f541eccfd3fb52b45b905c #429

Merged
merged 5 commits into from
Oct 11, 2023
Merged

update HACL to 1b30697fc2b0d8d5e2f541eccfd3fb52b45b905c #429

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
640362f
update HACL to 1a20576fc736d51e1ab3c317b46ba81560b75786
franziskuskiefer Oct 5, 2023
31cac37
no gcc-compat
franziskuskiefer Oct 5, 2023
90f97e7
disable warnings for benchmarks
franziskuskiefer Oct 5, 2023
079be45
only warnings for hacl
franziskuskiefer Oct 5, 2023
70b4970
update
franziskuskiefer Oct 11, 2023
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
6 changes: 3 additions & 3 deletions CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,12 +93,9 @@ if(NOT MSVC)
# -pedantic
# -Wconversion
# -Wsign-conversion
# -Werror=gcc-compat
$<$<CONFIG:DEBUG>:-g>
$<$<CONFIG:DEBUG>:-Og>
$<$<CONFIG:RELEASE>:-O3>
# $<$<CONFIG:RELEASE>:-g>
# $<$<CONFIG:RELEASE>:-Wno-deprecated-declarations>
)
endif()

Expand Down Expand Up @@ -337,6 +334,9 @@ configure_file(config/Config.h.in config.h)
# Now combine everything into the hacl library
# # Dynamic library
add_library(hacl SHARED ${SOURCES_std} ${VALE_OBJECTS})
if(NOT MSVC)
target_compile_options(hacl PRIVATE -Wsign-conversion -Wconversion -Wall -Wextra -pedantic)
endif()

if(TOOLCHAIN_CAN_COMPILE_VEC128 AND HACL_VEC128_O)
add_dependencies(hacl hacl_vec128)
Expand Down
45 changes: 27 additions & 18 deletions include/Hacl_RSAPSS.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,9 @@ extern "C" {
Sign a message `msg` and write the signature to `sgnt`.

@param a Hash algorithm to use. Allowed values for `a` are ...
* Spec_Hash_Definitions_SHA2_256,
* Spec_Hash_Definitions_SHA2_384, and
* Spec_Hash_Definitions_SHA2_512.
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param dBits Count of bits in `d` value.
Expand Down Expand Up @@ -75,7 +75,10 @@ Hacl_RSAPSS_rsapss_sign(
/**
Verify the signature `sgnt` of a message `msg`.

@param a Hash algorithm to use.
@param a Hash algorithm to use. Allowed values for `a` are ...
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`.
Expand Down Expand Up @@ -105,10 +108,10 @@ Load a public key from key parts.

@param modBits Count of bits in modulus (`n`).
@param eBits Count of bits in `e` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.

@return Returns an allocated public key. Note: caller must take care to `free()` the created key.
@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
*/
uint64_t
*Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb);
Expand All @@ -119,11 +122,11 @@ Load a secret key from key parts.
@param modBits Count of bits in modulus (`n`).
@param eBits Count of bits in `e` value.
@param dBits Count of bits in `d` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.

@return Returns an allocated secret key. Note: caller must take care to `free()` the created key.
@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
*/
uint64_t
*Hacl_RSAPSS_new_rsapss_load_skey(
Expand All @@ -138,13 +141,16 @@ uint64_t
/**
Sign a message `msg` and write the signature to `sgnt`.

@param a Hash algorithm to use.
@param a Hash algorithm to use. Allowed values for `a` are ...
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param dBits Count of bits in `d` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.
@param saltLen Length of salt.
@param salt Pointer to `saltLen` bytes where the salt is read from.
@param msgLen Length of message.
Expand Down Expand Up @@ -172,11 +178,14 @@ Hacl_RSAPSS_rsapss_skey_sign(
/**
Verify the signature `sgnt` of a message `msg`.

@param a Hash algorithm to use.
@param a Hash algorithm to use. Allowed values for `a` are ...
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
@param saltLen Length of salt.
@param sgntLen Length of signature.
@param sgnt Pointer to `sgntLen` bytes where the signature is read from.
Expand Down
4 changes: 4 additions & 0 deletions include/internal/Hacl_Bignum25519_51.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul(
FStar_UInt128_uint128 *uu___
)
{
KRML_HOST_IGNORE(uu___);
uint64_t f10 = f1[0U];
uint64_t f11 = f1[1U];
uint64_t f12 = f1[2U];
Expand Down Expand Up @@ -167,6 +168,7 @@ Hacl_Impl_Curve25519_Field51_fmul2(
FStar_UInt128_uint128 *uu___
)
{
KRML_HOST_IGNORE(uu___);
uint64_t f10 = f1[0U];
uint64_t f11 = f1[1U];
uint64_t f12 = f1[2U];
Expand Down Expand Up @@ -371,6 +373,7 @@ static inline void Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f
static inline void
Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
{
KRML_HOST_IGNORE(uu___);
uint64_t f0 = f[0U];
uint64_t f1 = f[1U];
uint64_t f2 = f[2U];
Expand Down Expand Up @@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint
static inline void
Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
{
KRML_HOST_IGNORE(uu___);
uint64_t f10 = f[0U];
uint64_t f11 = f[1U];
uint64_t f12 = f[2U];
Expand Down
45 changes: 27 additions & 18 deletions include/msvc/Hacl_RSAPSS.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,9 @@ extern "C" {
Sign a message `msg` and write the signature to `sgnt`.

@param a Hash algorithm to use. Allowed values for `a` are ...
* Spec_Hash_Definitions_SHA2_256,
* Spec_Hash_Definitions_SHA2_384, and
* Spec_Hash_Definitions_SHA2_512.
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param dBits Count of bits in `d` value.
Expand Down Expand Up @@ -75,7 +75,10 @@ Hacl_RSAPSS_rsapss_sign(
/**
Verify the signature `sgnt` of a message `msg`.

@param a Hash algorithm to use.
@param a Hash algorithm to use. Allowed values for `a` are ...
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`.
Expand Down Expand Up @@ -105,10 +108,10 @@ Load a public key from key parts.

@param modBits Count of bits in modulus (`n`).
@param eBits Count of bits in `e` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.

@return Returns an allocated public key. Note: caller must take care to `free()` the created key.
@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
*/
uint64_t
*Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb);
Expand All @@ -119,11 +122,11 @@ Load a secret key from key parts.
@param modBits Count of bits in modulus (`n`).
@param eBits Count of bits in `e` value.
@param dBits Count of bits in `d` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.

@return Returns an allocated secret key. Note: caller must take care to `free()` the created key.
@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
*/
uint64_t
*Hacl_RSAPSS_new_rsapss_load_skey(
Expand All @@ -138,13 +141,16 @@ uint64_t
/**
Sign a message `msg` and write the signature to `sgnt`.

@param a Hash algorithm to use.
@param a Hash algorithm to use. Allowed values for `a` are ...
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param dBits Count of bits in `d` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.
@param saltLen Length of salt.
@param salt Pointer to `saltLen` bytes where the salt is read from.
@param msgLen Length of message.
Expand Down Expand Up @@ -172,11 +178,14 @@ Hacl_RSAPSS_rsapss_skey_sign(
/**
Verify the signature `sgnt` of a message `msg`.

@param a Hash algorithm to use.
@param a Hash algorithm to use. Allowed values for `a` are ...
- Spec_Hash_Definitions_SHA2_256,
- Spec_Hash_Definitions_SHA2_384, and
- Spec_Hash_Definitions_SHA2_512.
@param modBits Count of bits in the modulus (`n`).
@param eBits Count of bits in `e` value.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
@param saltLen Length of salt.
@param sgntLen Length of signature.
@param sgnt Pointer to `sgntLen` bytes where the signature is read from.
Expand Down
4 changes: 4 additions & 0 deletions include/msvc/internal/Hacl_Bignum25519_51.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul(
FStar_UInt128_uint128 *uu___
)
{
KRML_HOST_IGNORE(uu___);
uint64_t f10 = f1[0U];
uint64_t f11 = f1[1U];
uint64_t f12 = f1[2U];
Expand Down Expand Up @@ -167,6 +168,7 @@ Hacl_Impl_Curve25519_Field51_fmul2(
FStar_UInt128_uint128 *uu___
)
{
KRML_HOST_IGNORE(uu___);
uint64_t f10 = f1[0U];
uint64_t f11 = f1[1U];
uint64_t f12 = f1[2U];
Expand Down Expand Up @@ -371,6 +373,7 @@ static inline void Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f
static inline void
Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
{
KRML_HOST_IGNORE(uu___);
uint64_t f0 = f[0U];
uint64_t f1 = f[1U];
uint64_t f2 = f[2U];
Expand Down Expand Up @@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint
static inline void
Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
{
KRML_HOST_IGNORE(uu___);
uint64_t f10 = f[0U];
uint64_t f11 = f[1U];
uint64_t f12 = f[2U];
Expand Down
6 changes: 3 additions & 3 deletions info.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
The code was generated with the following toolchain.
F* version: 155853a14336aa0713dba7db5408f4c8ab512a06
KaRaMeL version: db63c1de17565be0ec4989f58532717a04e3ff40
HACL* version: ad60c9d98c9ce8f6a4fa13090511fa4b3a2c137b
F* version: bc622701c668f6b4092760879372968265d4a4e1
KaRaMeL version: 7cffd27cfefbd220e986e561e8d350f043609f76
HACL* version: 1b30697fc2b0d8d5e2f541eccfd3fb52b45b905c
Vale version: 0.3.19
8 changes: 8 additions & 0 deletions karamel/include/krml/internal/target.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,14 @@
# define KRML_HOST_IGNORE(x) (void)(x)
#endif

#ifndef KRML_MAYBE_UNUSED
# if defined(__GNUC__)
# define KRML_MAYBE_UNUSED __attribute__((unused))
# else
# define KRML_MAYBE_UNUSED
# endif
#endif

#ifndef KRML_NOINLINE
# if defined(_MSC_VER)
# define KRML_NOINLINE __declspec(noinline)
Expand Down
56 changes: 0 additions & 56 deletions karamel/krmllib/dist/minimal/Makefile.basic
View file
Open in desktop

This file was deleted.

5 changes: 0 additions & 5 deletions karamel/krmllib/dist/minimal/Makefile.include
View file
Open in desktop

This file was deleted.

4 changes: 2 additions & 2 deletions karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,15 +110,15 @@ inline static uint128_t FStar_UInt128_mul_wide(uint64_t x, uint64_t y) {
inline static uint128_t FStar_UInt128_eq_mask(uint128_t x, uint128_t y) {
uint64_t mask =
FStar_UInt64_eq_mask((uint64_t)(x >> 64), (uint64_t)(y >> 64)) &
FStar_UInt64_eq_mask(x, y);
FStar_UInt64_eq_mask((uint64_t)x, (uint64_t)y);
return ((uint128_t)mask) << 64 | mask;
}

inline static uint128_t FStar_UInt128_gte_mask(uint128_t x, uint128_t y) {
uint64_t mask =
(FStar_UInt64_gte_mask(x >> 64, y >> 64) &
~(FStar_UInt64_eq_mask(x >> 64, y >> 64))) |
(FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask(x, y));
(FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask((uint64_t)x, (uint64_t)y));
return ((uint128_t)mask) << 64 | mask;
}

Expand Down
11 changes: 0 additions & 11 deletions karamel/krmllib/dist/minimal/libkrmllib.def
View file
Open in desktop

This file was deleted.

Loading