Skip to content

Various small fixes and improvements #1468

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

Open
mkannwischer wants to merge 7 commits into
base: main
Choose a base branch
from
Open

Various small fixes and improvements #1468

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
e8ce970
params.h: Reject invalid MLD_CONFIG_PARAMETER_SET values
mkannwischer Oct 13, 2026
29f5f8b
prepare_domain_separation_prefix: Align declaration guard with defini…
mkannwischer Oct 19, 2026
2ba5308
prepare_domain_separation_prefix: Cover ctxlen > 255 in the contract
mkannwischer Oct 19, 2026
02d6258
prepare_domain_separation_prefix: Do not check ph for NULL
mkannwischer Oct 19, 2026
4b0424a
Guard helpers of pk_from_sk by MLD_CONFIG_CORE_API_ONLY
mkannwischer Oct 13, 2026
e2e5cb3
rv32im: Reject the backend on targets other than RV32 with M
mkannwischer Oct 13, 2026
a238db9
armv81m: Check the MVE capability in the x4 Keccak backend
mkannwischer Oct 13, 2026
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
12 changes: 12 additions & 0 deletions dev/fips202/armv81m/mve.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,10 @@ int mld_keccak_f1600_x4_native_impl(uint64_t *state);
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
return mld_keccak_f1600_x4_native_impl(state);
}

Expand All @@ -44,6 +48,10 @@ static MLD_INLINE int mld_keccakf1600_xor_bytes_x4_native(
const uint8_t *data2, const uint8_t *data3, unsigned offset,
unsigned length)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_keccak_f1600_x4_state_xor_bytes_asm(state, data0, data1, data2, data3,
offset, length);
return MLD_NATIVE_FUNC_SUCCESS;
Expand All @@ -57,6 +65,10 @@ static MLD_INLINE int mld_keccakf1600_extract_bytes_x4_native(
uint64_t *state, uint8_t *data0, uint8_t *data1, uint8_t *data2,
uint8_t *data3, unsigned offset, unsigned length)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_keccak_f1600_x4_state_extract_bytes_asm(state, data0, data1, data2, data3,
offset, length);
return MLD_NATIVE_FUNC_SUCCESS;
Expand Down
4 changes: 4 additions & 0 deletions dev/riscv32/fastmul.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@
#ifndef MLD_DEV_RISCV32_FASTMUL_H
#define MLD_DEV_RISCV32_FASTMUL_H

#if !defined(MLD_SYS_RISCV32_M)

@hanno-becker hanno-becker Oct 18, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, we don't have this for the other backends, though... we should be consistent, whatever we do.

@mkannwischer mkannwischer Oct 19, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not aware of a case before that a backend can accidentally be assembled for an unsupported architecture instead of failing to assemble at all. If we do have more cases like that, we should guard it equally.

The x86_64 FIPS202 backend has a similar guard, but I think that's actually not needed:

mldsa-native/mldsa/src/fips202/native/x86_64/src/fips202_native_x86_64.h

Line 16 in 6daba60

#error Expecting a little-endian platform

#error This backend can only be used on RV32 targets with the M extension.
#endif

/*
* Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
* ILP32D family of ABIs. This is the default arithmetic backend selected by
Expand Down
4 changes: 4 additions & 0 deletions dev/riscv32/slowmul.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@
#ifndef MLD_DEV_RISCV32_SLOWMUL_H
#define MLD_DEV_RISCV32_SLOWMUL_H

#if !defined(MLD_SYS_RISCV32_M)
#error This backend can only be used on RV32 targets with the M extension.
#endif

/*
* Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
* ILP32D family of ABIs. Select this profile explicitly through
Expand Down
6 changes: 4 additions & 2 deletions mldsa/mldsa_native.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -793,6 +793,7 @@ int MLD_API_NAMESPACE(verify_pre_hash_shake256)(
#endif /* !MLD_CONFIG_CORE_API_ONLY */

#if !defined(MLD_CONFIG_CORE_API_ONLY)
#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
/**
* Prepare domain separation prefix for ML-DSA signing.
*
Expand Down Expand Up @@ -828,14 +829,15 @@ int MLD_API_NAMESPACE(verify_pre_hash_shake256)(
* @return The total length of the formatted prefix, or 0 on error.
* Errors are:
* - The context string exceeded 255 bytes.
* - For HashML-DSA: hashalg was unsupported, ph was NULL, or phlen
* did not match the output length of hashalg.
* - For HashML-DSA: hashalg was unsupported, or phlen did not match
* the output length of hashalg.
*/
MLD_API_QUALIFIER
MLD_API_MUST_CHECK_RETURN_VALUE
size_t MLD_API_NAMESPACE(prepare_domain_separation_prefix)(
uint8_t prefix[MLD_DOMAIN_SEPARATION_MAX_BYTES], const uint8_t *ph,
size_t phlen, const uint8_t *ctx, size_t ctxlen, int hashalg);
#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */

#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
/**
Expand Down
12 changes: 12 additions & 0 deletions mldsa/src/fips202/native/armv81m/mve.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,10 @@ int mld_keccak_f1600_x4_native_impl(uint64_t *state);
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
return mld_keccak_f1600_x4_native_impl(state);
}

Expand All @@ -44,6 +48,10 @@ static MLD_INLINE int mld_keccakf1600_xor_bytes_x4_native(
const uint8_t *data2, const uint8_t *data3, unsigned offset,
unsigned length)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_keccak_f1600_x4_state_xor_bytes_asm(state, data0, data1, data2, data3,
offset, length);
return MLD_NATIVE_FUNC_SUCCESS;
Expand All @@ -57,6 +65,10 @@ static MLD_INLINE int mld_keccakf1600_extract_bytes_x4_native(
uint64_t *state, uint8_t *data0, uint8_t *data1, uint8_t *data2,
uint8_t *data3, unsigned offset, unsigned length)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_keccak_f1600_x4_state_extract_bytes_asm(state, data0, data1, data2, data3,
offset, length);
return MLD_NATIVE_FUNC_SUCCESS;
Expand Down
4 changes: 4 additions & 0 deletions mldsa/src/native/rv32im/fastmul.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@
#ifndef MLD_NATIVE_RV32IM_FASTMUL_H
#define MLD_NATIVE_RV32IM_FASTMUL_H

#if !defined(MLD_SYS_RISCV32_M)
#error This backend can only be used on RV32 targets with the M extension.
#endif

/*
* Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
* ILP32D family of ABIs. This is the default arithmetic backend selected by
Expand Down
4 changes: 4 additions & 0 deletions mldsa/src/native/rv32im/slowmul.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@
#ifndef MLD_NATIVE_RV32IM_SLOWMUL_H
#define MLD_NATIVE_RV32IM_SLOWMUL_H

#if !defined(MLD_SYS_RISCV32_M)
#error This backend can only be used on RV32 targets with the M extension.
#endif

/*
* Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
* ILP32D family of ABIs. Select this profile explicitly through
Expand Down
5 changes: 4 additions & 1 deletion mldsa/src/params.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,10 @@
/* check-magic: 96 == MLDSA_N * 3 / 8 */
#define MLDSA_POLYETA_PACKEDBYTES 96

#endif /* MLD_CONFIG_PARAMETER_SET == 87 */
#else /* MLD_CONFIG_PARAMETER_SET == 87 */
#error Invalid value for MLD_CONFIG_PARAMETER_SET. Must be 44, 65, or 87.
#endif /* MLD_CONFIG_PARAMETER_SET != 44 && MLD_CONFIG_PARAMETER_SET != 65 && \
MLD_CONFIG_PARAMETER_SET != 87 */

#define MLDSA_POLYT1_PACKEDBITS 10
/* check-magic: 320 == MLDSA_N * MLDSA_POLYT1_PACKEDBITS / 8 */
Expand Down
7 changes: 7 additions & 0 deletions mldsa/src/poly.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -918,6 +918,10 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT0_PACKEDBYTES])
}
#endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \
(!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
!defined(MLD_CONFIG_CORE_API_ONLY)) || \
defined(MLD_UNIT_TEST)
MLD_STATIC_TESTABLE uint32_t mld_poly_chknorm_c(const mld_poly *a, int32_t B)
__contract__(
requires(memory_no_alias(a, sizeof(mld_poly)))
Expand Down Expand Up @@ -1004,6 +1008,9 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
#endif /* MLD_USE_NATIVE_POLY_CHKNORM */
return mld_poly_chknorm_c(a, B);
}
#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API || \
(!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
Expand Down
7 changes: 7 additions & 0 deletions mldsa/src/poly.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -385,6 +385,10 @@ __contract__(
);
#endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \
(!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
!defined(MLD_CONFIG_CORE_API_ONLY)) || \
defined(MLD_UNIT_TEST)
#define mld_poly_chknorm MLD_NAMESPACE(poly_chknorm)
/**
* Check infinity norm of polynomial against given bound. Assumes input
Expand Down Expand Up @@ -413,6 +417,9 @@ __contract__(
ensures(return_value == 0 || return_value == 0xFFFFFFFF)
ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B))
);
#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API || \
(!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
Expand Down
22 changes: 13 additions & 9 deletions mldsa/src/polyvec.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,8 +206,9 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
}
#endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \
defined(MLD_UNIT_TEST)
#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
!defined(MLD_CONFIG_CORE_API_ONLY)) || \
!defined(MLD_CONFIG_NO_VERIFY_API) || defined(MLD_UNIT_TEST)
MLD_INTERNAL_API
uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound)
{
Expand All @@ -232,8 +233,8 @@ uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound)
}
return t;
}
#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API || \
MLD_UNIT_TEST */
#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
!MLD_CONFIG_NO_VERIFY_API || MLD_UNIT_TEST */

/**************************************************************/
/************ Vectors of polynomials of length MLDSA_K **************/
Expand Down Expand Up @@ -334,7 +335,7 @@ void mld_polyveck_invntt_tomont(mld_polyveck *v)
}
#endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
#if !defined(MLD_CONFIG_NO_KEYPAIR_API) && !defined(MLD_CONFIG_CORE_API_ONLY)
MLD_INTERNAL_API
uint32_t mld_polyveck_unpack_eta_chknorm(
const uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES], int32_t bound,
Expand Down Expand Up @@ -362,7 +363,7 @@ uint32_t mld_polyveck_unpack_eta_chknorm(
return t;
}

#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
#endif /* !MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY */

#if !defined(MLD_CONFIG_NO_SIGN_API)
MLD_INTERNAL_API
Expand Down Expand Up @@ -394,8 +395,10 @@ void mld_polyveck_decompose_pack_w1(
}
#endif /* !MLD_CONFIG_NO_SIGN_API */

#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \
(!defined(MLD_CONFIG_NO_SIGN_API) && \
#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
!defined(MLD_CONFIG_CORE_API_ONLY)) || \
((!defined(MLD_CONFIG_NO_KEYPAIR_API) || \
!defined(MLD_CONFIG_NO_SIGN_API)) && \
(!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)))
MLD_INTERNAL_API
void mld_polyvecl_unpack_eta(
Expand All @@ -410,7 +413,8 @@ void mld_polyvecl_unpack_eta(
mld_assert_bound_2d(p->vec, MLDSA_L, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND,
MLDSA_ETA + 1);
}
#endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_SIGN_API && \
#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
((!MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_SIGN_API) && \
(!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) */

#if !defined(MLD_CONFIG_NO_VERIFY_API)
Expand Down
20 changes: 13 additions & 7 deletions mldsa/src/polyvec.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,9 @@ __contract__(
);
#endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
!defined(MLD_CONFIG_CORE_API_ONLY)) || \
!defined(MLD_CONFIG_NO_VERIFY_API)
#define mld_polyvecl_chknorm MLD_NAMESPACE_KL(polyvecl_chknorm)
/**
* Check infinity norm of polynomials in vector of length MLDSA_L. Assumes
Expand All @@ -147,7 +149,8 @@ __contract__(
ensures(return_value == 0 || return_value == 0xFFFFFFFF)
ensures((return_value == 0) == forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, B)))
);
#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */
#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
!MLD_CONFIG_NO_VERIFY_API */

/** Vector of MLDSA_K polynomials. */
typedef struct
Expand Down Expand Up @@ -238,7 +241,7 @@ __contract__(
);
#endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */

#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
#if !defined(MLD_CONFIG_NO_KEYPAIR_API) && !defined(MLD_CONFIG_CORE_API_ONLY)
#define mld_polyveck_unpack_eta_chknorm \
MLD_NAMESPACE_KL(polyveck_unpack_eta_chknorm)
/**
Expand Down Expand Up @@ -266,7 +269,7 @@ __contract__(
ensures(return_value == 0 || return_value == 0xFFFFFFFF)
);

#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
#endif /* !MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY */

#if !defined(MLD_CONFIG_NO_SIGN_API)
#define mld_polyveck_decompose_pack_w1 \
Expand Down Expand Up @@ -315,8 +318,10 @@ __contract__(
);
#endif /* !MLD_CONFIG_NO_SIGN_API */

#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \
(!defined(MLD_CONFIG_NO_SIGN_API) && \
#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
!defined(MLD_CONFIG_CORE_API_ONLY)) || \
((!defined(MLD_CONFIG_NO_KEYPAIR_API) || \
!defined(MLD_CONFIG_NO_SIGN_API)) && \
(!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)))
#define mld_polyvecl_unpack_eta MLD_NAMESPACE_KL(polyvecl_unpack_eta)
/**
Expand All @@ -335,7 +340,8 @@ __contract__(
ensures(forall(k1, 0, MLDSA_L,
array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)))
);
#endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_SIGN_API && \
#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
((!MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_SIGN_API) && \
(!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) */

#if !defined(MLD_CONFIG_NO_VERIFY_API)
Expand Down
2 changes: 1 addition & 1 deletion mldsa/src/sign.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1648,7 +1648,7 @@ size_t mld_prepare_domain_separation_prefix(

if (hashalg != MLD_PREHASH_NONE)
{
if (ph == NULL || mld_validate_hash_length(hashalg, phlen) != 0)
if (mld_validate_hash_length(hashalg, phlen) != 0)
{
return 0;
}
Expand Down
7 changes: 4 additions & 3 deletions mldsa/src/sign.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -787,22 +787,23 @@ __contract__(
* @return The total length of the formatted prefix, or 0 on error.
* Errors are:
* - The context string exceeded 255 bytes.
* - For HashML-DSA: hashalg was unsupported, ph was NULL, or phlen
* did not match the output length of hashalg.
* - For HashML-DSA: hashalg was unsupported, or phlen did not match
* the output length of hashalg.
*/
MLD_MUST_CHECK_RETURN_VALUE
MLD_EXTERNAL_API
size_t mld_prepare_domain_separation_prefix(
uint8_t prefix[MLD_DOMAIN_SEPARATION_MAX_BYTES], const uint8_t *ph,
size_t phlen, const uint8_t *ctx, size_t ctxlen, int hashalg)
__contract__(
requires(ctxlen <= 255)
requires(ctxlen <= MLD_MAX_BUFFER_SIZE)
requires(phlen <= MLD_MAX_BUFFER_SIZE)
requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen))
requires(hashalg == MLD_PREHASH_NONE || memory_no_alias(ph, phlen))
requires(memory_no_alias(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES))
assigns(memory_slice(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES))
ensures(return_value <= MLD_DOMAIN_SEPARATION_MAX_BYTES)
ensures(ctxlen > 255 ==> return_value == 0)
);
#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */

Expand Down
1 change: 1 addition & 0 deletions proofs/cbmc/intt_native_rv32im_fastmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ HARNESS_FILE = intt_native_rv32im_fastmul_harness
PROOF_UID = intt_native_rv32im_fastmul

DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
DEFINES += -DMLD_SYS_RISCV32_M
DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/fastmul.h\""
DEFINES += -DMLD_CHECK_APIS

Expand Down
1 change: 1 addition & 0 deletions proofs/cbmc/intt_native_rv32im_slowmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ HARNESS_FILE = intt_native_rv32im_slowmul_harness
PROOF_UID = intt_native_rv32im_slowmul

DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
DEFINES += -DMLD_SYS_RISCV32_M
DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/slowmul.h\""
DEFINES += -DMLD_CHECK_APIS

Expand Down
1 change: 1 addition & 0 deletions proofs/cbmc/ntt_native_rv32im_fastmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ HARNESS_FILE = ntt_native_rv32im_fastmul_harness
PROOF_UID = ntt_native_rv32im_fastmul

DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
DEFINES += -DMLD_SYS_RISCV32_M
DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/fastmul.h\""
DEFINES += -DMLD_CHECK_APIS

Expand Down
1 change: 1 addition & 0 deletions proofs/cbmc/ntt_native_rv32im_slowmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ HARNESS_FILE = ntt_native_rv32im_slowmul_harness
PROOF_UID = ntt_native_rv32im_slowmul

DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
DEFINES += -DMLD_SYS_RISCV32_M
DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/slowmul.h\""
DEFINES += -DMLD_CHECK_APIS

Expand Down
1 change: 1 addition & 0 deletions proofs/cbmc/pointwise_native_rv32im_fastmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ HARNESS_FILE = pointwise_native_rv32im_fastmul_harness
PROOF_UID = pointwise_native_rv32im_fastmul

DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
DEFINES += -DMLD_SYS_RISCV32_M
DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/fastmul.h\""
DEFINES += -DMLD_CHECK_APIS

Expand Down
1 change: 1 addition & 0 deletions proofs/cbmc/pointwise_native_rv32im_slowmul/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ HARNESS_FILE = pointwise_native_rv32im_slowmul_harness
PROOF_UID = pointwise_native_rv32im_slowmul

DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
DEFINES += -DMLD_SYS_RISCV32_M
DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/slowmul.h\""
DEFINES += -DMLD_CHECK_APIS

Expand Down
Loading