Skip to content

Standardize on signed integers in quantifiers and loops. #706

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

Draft
rod-chapman wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

Standardize on signed integers in quantifiers and loops. #706

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4cd985b
Standardize on signed integers in quantifiers and loops.
rod-chapman Nov 12, 2025
d713e35
Corrections following rebase and re-generate files
rod-chapman Dec 1, 2025
a5ae4ce
More corrections following rebase
rod-chapman Dec 3, 2025
d1c3517
Correct harnesses and re-introduce >= 0 preconditions for int params
rod-chapman Dec 3, 2025
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 dev/aarch64_clean/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@


#if !defined(__ASSEMBLER__)
#include <stddef.h>
#include "../api.h"
#include "src/arith_native_aarch64.h"

Expand All @@ -49,25 +50,24 @@ static MLD_INLINE int mld_intt_native(int32_t data[MLDSA_N])
return MLD_NATIVE_FUNC_SUCCESS;
}

static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
const uint8_t *buf,
unsigned buflen)
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, int len,
const uint8_t *buf, int buflen)
{
if (len != MLDSA_N ||
buflen % 24 != 0) /* NEON support is mandatory for AArch64 */
{
return MLD_NATIVE_FUNC_FALLBACK;
}

/* Safety: outlen is at most MLDSA_N, hence, this cast is safe. */
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)mld_rej_uniform_asm(r, buf, buflen, mld_rej_uniform_table);
}

static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, int len,
const uint8_t *buf,
unsigned buflen)
int buflen)
{
unsigned int outlen;
int32_t outlen;
/* AArch64 implementation assumes specific buffer lengths */
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
{
Expand All @@ -82,16 +82,16 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
*/
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
outlen = mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)outlen;
}

static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, int len,
const uint8_t *buf,
unsigned buflen)
int buflen)
{
unsigned int outlen;
int32_t outlen;
/* AArch64 implementation assumes specific buffer lengths */
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
{
Expand All @@ -106,7 +106,7 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
*/
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
outlen = mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)outlen;
}
Expand Down
10 changes: 5 additions & 5 deletions dev/aarch64_clean/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,16 +56,16 @@ void mld_ntt_asm(int32_t *, const int32_t *, const int32_t *);
void mld_intt_asm(int32_t *, const int32_t *, const int32_t *);

#define mld_rej_uniform_asm MLD_NAMESPACE(rej_uniform_asm)
uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, unsigned buflen,
uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
const uint8_t *table);

#define mld_rej_uniform_eta2_asm MLD_NAMESPACE(rej_uniform_eta2_asm)
unsigned mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf,
unsigned buflen, const uint8_t *table);
int32_t mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
const uint8_t *table);

#define mld_rej_uniform_eta4_asm MLD_NAMESPACE(rej_uniform_eta4_asm)
unsigned mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
unsigned buflen, const uint8_t *table);
int32_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
const uint8_t *table);

#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0, const int32_t *a);
Expand Down
24 changes: 12 additions & 12 deletions dev/aarch64_opt/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@


#if !defined(__ASSEMBLER__)
#include <stddef.h>
#include "../api.h"
#include "src/arith_native_aarch64.h"

Expand All @@ -49,25 +50,24 @@ static MLD_INLINE int mld_intt_native(int32_t data[MLDSA_N])
return MLD_NATIVE_FUNC_SUCCESS;
}

static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
const uint8_t *buf,
unsigned buflen)
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, int len,
const uint8_t *buf, int buflen)
{
if (len != MLDSA_N ||
buflen % 24 != 0) /* NEON support is mandatory for AArch64 */
{
return MLD_NATIVE_FUNC_FALLBACK;
}

/* Safety: outlen is at most MLDSA_N, hence, this cast is safe. */
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)mld_rej_uniform_asm(r, buf, buflen, mld_rej_uniform_table);
}

static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, int len,
const uint8_t *buf,
unsigned buflen)
int buflen)
{
unsigned int outlen;
int32_t outlen;
/* AArch64 implementation assumes specific buffer lengths */
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
{
Expand All @@ -82,16 +82,16 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
*/
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
outlen = mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)outlen;
}

static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, int len,
const uint8_t *buf,
unsigned buflen)
int buflen)
{
unsigned int outlen;
int32_t outlen;
/* AArch64 implementation assumes specific buffer lengths */
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
{
Expand All @@ -106,7 +106,7 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
*/
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
outlen = mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)outlen;
}
Expand Down
10 changes: 5 additions & 5 deletions dev/aarch64_opt/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,16 +56,16 @@ void mld_ntt_asm(int32_t *, const int32_t *, const int32_t *);
void mld_intt_asm(int32_t *, const int32_t *, const int32_t *);

#define mld_rej_uniform_asm MLD_NAMESPACE(rej_uniform_asm)
uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, unsigned buflen,
uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
const uint8_t *table);

#define mld_rej_uniform_eta2_asm MLD_NAMESPACE(rej_uniform_eta2_asm)
unsigned mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf,
unsigned buflen, const uint8_t *table);
int32_t mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
const uint8_t *table);

#define mld_rej_uniform_eta4_asm MLD_NAMESPACE(rej_uniform_eta4_asm)
unsigned mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
unsigned buflen, const uint8_t *table);
int32_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
const uint8_t *table);

#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0, const int32_t *a);
Expand Down
22 changes: 11 additions & 11 deletions dev/x86_64/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7

#if !defined(__ASSEMBLER__)
#include <stddef.h>
#include <string.h>
#include "../../common.h"
#include "../api.h"
Expand Down Expand Up @@ -64,9 +65,8 @@ static MLD_INLINE int mld_intt_native(int32_t data[MLDSA_N])
return MLD_NATIVE_FUNC_SUCCESS;
}

static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
const uint8_t *buf,
unsigned buflen)
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, int len,
const uint8_t *buf, int buflen)
{
/* AVX2 implementation assumes specific buffer lengths */
if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2) || len != MLDSA_N ||
Expand All @@ -79,11 +79,11 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
return (int)mld_rej_uniform_avx2(r, buf);
}

static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, int len,
const uint8_t *buf,
unsigned buflen)
int buflen)
{
unsigned int outlen;
int32_t outlen;
/* AVX2 implementation assumes specific buffer lengths */
if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2) || len != MLDSA_N ||
buflen != MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN)
Expand All @@ -100,16 +100,16 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
*/
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
outlen = mld_rej_uniform_eta2_avx2(r, buf);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)outlen;
}

static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, int len,
const uint8_t *buf,
unsigned buflen)
int buflen)
{
unsigned int outlen;
int32_t outlen;
/* AVX2 implementation assumes specific buffer lengths */
if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2) || len != MLDSA_N ||
buflen != MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN)
Expand All @@ -126,7 +126,7 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
*/
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
outlen = mld_rej_uniform_eta4_avx2(r, buf);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
return (int)outlen;
}
Expand Down
8 changes: 4 additions & 4 deletions dev/x86_64/src/arith_native_x86_64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,15 +43,15 @@ void mld_invntt_avx2(__m256i *r, const __m256i *mld_qdata);
void mld_nttunpack_avx2(__m256i *r);

#define mld_rej_uniform_avx2 MLD_NAMESPACE(mld_rej_uniform_avx2)
unsigned mld_rej_uniform_avx2(int32_t *r,
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN]);
int32_t mld_rej_uniform_avx2(int32_t *r,
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN]);

#define mld_rej_uniform_eta2_avx2 MLD_NAMESPACE(mld_rej_uniform_eta2_avx2)
unsigned mld_rej_uniform_eta2_avx2(
int32_t mld_rej_uniform_eta2_avx2(
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN]);

#define mld_rej_uniform_eta4_avx2 MLD_NAMESPACE(mld_rej_uniform_eta4_avx2)
unsigned mld_rej_uniform_eta4_avx2(
int32_t mld_rej_uniform_eta4_avx2(
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN]);

#define mld_poly_decompose_32_avx2 MLD_NAMESPACE(mld_poly_decompose_32_avx2)
Expand Down
6 changes: 3 additions & 3 deletions dev/x86_64/src/rej_uniform_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@
* frontend to perform the unintuitive padding.
*/

unsigned int mld_rej_uniform_avx2(
int32_t *MLD_RESTRICT r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN])
int32_t mld_rej_uniform_avx2(int32_t *MLD_RESTRICT r,
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN])
{
unsigned int ctr, pos;
uint32_t good;
Expand Down Expand Up @@ -116,7 +116,7 @@ unsigned int mld_rej_uniform_avx2(
}
}

return ctr;
return (int32_t)ctr;
}

#else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \
Expand Down
4 changes: 2 additions & 2 deletions dev/x86_64/src/rej_uniform_eta2_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@
* rej_eta_avx and supports multiple values for ETA via preprocessor
* conditionals. We move the conditionals to the frontend.
*/
unsigned int mld_rej_uniform_eta2_avx2(
int32_t mld_rej_uniform_eta2_avx2(
int32_t *MLD_RESTRICT r,
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN])
{
Expand Down Expand Up @@ -139,7 +139,7 @@ unsigned int mld_rej_uniform_eta2_avx2(
}
}

return ctr;
return (int32_t)ctr;
}

#else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \
Expand Down
4 changes: 2 additions & 2 deletions dev/x86_64/src/rej_uniform_eta4_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@
* conditionals. We move the conditionals to the frontend.
*/

unsigned int mld_rej_uniform_eta4_avx2(
int32_t mld_rej_uniform_eta4_avx2(
int32_t *MLD_RESTRICT r,
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN])
{
Expand Down Expand Up @@ -123,7 +123,7 @@ unsigned int mld_rej_uniform_eta4_avx2(
}
}

return ctr;
return (int32_t)ctr;
}

#else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \
Expand Down
6 changes: 3 additions & 3 deletions mldsa/src/cbmc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,14 +93,14 @@
#define forall(qvar, qvar_lb, qvar_ub, predicate) \
__CPROVER_forall \
{ \
unsigned qvar; \
signed int qvar; \
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \
}

#define exists(qvar, qvar_lb, qvar_ub, predicate) \
__CPROVER_exists \
{ \
unsigned qvar; \
signed int qvar; \
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \
}
/* clang-format on */
Expand All @@ -119,7 +119,7 @@
value_lb, value_ub) \
__CPROVER_forall \
{ \
unsigned qvar; \
signed int qvar; \
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
(((int)(value_lb) <= ((array_var)[(qvar)])) && \
(((array_var)[(qvar)]) < (int)(value_ub))) \
Expand Down
4 changes: 2 additions & 2 deletions mldsa/src/debug.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,11 +30,11 @@ void mld_debug_check_assert(const char *file, int line, const int val)
}

void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
unsigned len, int64_t lower_bound_exclusive,
int len, int64_t lower_bound_exclusive,
int64_t upper_bound_exclusive)
{
int err = 0;
unsigned i;
int i;
for (i = 0; i < len; i++)
{
int32_t val = ptr[i];
Expand Down
2 changes: 1 addition & 1 deletion mldsa/src/debug.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ void mld_debug_check_assert(const char *file, int line, const int val);
**************************************************/
#define mld_debug_check_bounds MLD_NAMESPACE(mldsa_debug_check_bounds)
void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
unsigned len, int64_t lower_bound_exclusive,
int len, int64_t lower_bound_exclusive,
int64_t upper_bound_exclusive);

/* Check assertion, calling exit() upon failure
Expand Down
Loading