Skip to content

Commit a0a8f06

Browse files
rod-chapmanrod-chapman
committed
Standardize on signed integers in quantifiers and loops.
Specifically, use signed "int" for: 1. for loop counters 2. quantified expressions 3. variables and struct fields that count or index into arrays 4. formal parameters for array indexes, offsets and counts Additionally, strengthen pre-conditions on polyvecl_add() and polyveck_add() to stabilize proof of those functions for all parameter sets. Signed-off-by: Rod Chapman <[email protected]>
1 parent c6d7c93 commit a0a8f06

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

54 files changed

+467
-464
lines changed

‎dev/aarch64_clean/meta.h‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@
3232

3333

3434
#if !defined(__ASSEMBLER__)
35+
#include <stddef.h>
3536
#include "src/arith_native_aarch64.h"
3637

3738
static MLD_INLINE void mld_ntt_native(int32_t data[MLDSA_N])
@@ -46,24 +47,23 @@ static MLD_INLINE void mld_intt_native(int32_t data[MLDSA_N])
4647
mld_aarch64_intt_zetas_layer123456);
4748
}
4849

49-
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
50-
const uint8_t *buf,
51-
unsigned buflen)
50+
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, int len,
51+
const uint8_t *buf, int buflen)
5252
{
5353
if (len != MLDSA_N || buflen % 24 != 0)
5454
{
5555
return -1;
5656
}
5757

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

62-
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
62+
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, int len,
6363
const uint8_t *buf,
64-
unsigned buflen)
64+
int buflen)
6565
{
66-
unsigned int outlen;
66+
int32_t outlen;
6767
/* AArch64 implementation assumes specific buffer lengths */
6868
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
6969
{
@@ -78,16 +78,16 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
7878
*/
7979
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
8080
outlen = mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
81-
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
81+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
8282
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
8383
return (int)outlen;
8484
}
8585

86-
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
86+
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, int len,
8787
const uint8_t *buf,
88-
unsigned buflen)
88+
int buflen)
8989
{
90-
unsigned int outlen;
90+
int32_t outlen;
9191
/* AArch64 implementation assumes specific buffer lengths */
9292
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
9393
{
@@ -102,7 +102,7 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
102102
*/
103103
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
104104
outlen = mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
105-
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
105+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
106106
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
107107
return (int)outlen;
108108
}

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -56,16 +56,16 @@ void mld_ntt_asm(int32_t *, const int32_t *, const int32_t *);
5656
void mld_intt_asm(int32_t *, const int32_t *, const int32_t *);
5757

5858
#define mld_rej_uniform_asm MLD_NAMESPACE(rej_uniform_asm)
59-
uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, unsigned buflen,
59+
uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
6060
const uint8_t *table);
6161

6262
#define mld_rej_uniform_eta2_asm MLD_NAMESPACE(rej_uniform_eta2_asm)
63-
unsigned mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf,
64-
unsigned buflen, const uint8_t *table);
63+
int32_t mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
64+
const uint8_t *table);
6565

6666
#define mld_rej_uniform_eta4_asm MLD_NAMESPACE(rej_uniform_eta4_asm)
67-
unsigned mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
68-
unsigned buflen, const uint8_t *table);
67+
int32_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf, int32_t buflen,
68+
const uint8_t *table);
6969

7070
#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
7171
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0, const int32_t *a);

‎dev/x86_64/meta.h‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7
3232

3333
#if !defined(__ASSEMBLER__)
34+
#include <stddef.h>
3435
#include <string.h>
3536
#include "../../common.h"
3637
#include "src/arith_native_x86_64.h"
@@ -49,9 +50,8 @@ static MLD_INLINE void mld_intt_native(int32_t data[MLDSA_N])
4950
mld_invntt_avx2((__m256i *)data, mld_qdata.vec);
5051
}
5152

52-
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
53-
const uint8_t *buf,
54-
unsigned buflen)
53+
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, int len,
54+
const uint8_t *buf, int buflen)
5555
{
5656
/* AVX2 implementation assumes specific buffer lengths */
5757
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_BUFLEN)
@@ -63,11 +63,11 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
6363
return (int)mld_rej_uniform_avx2(r, buf);
6464
}
6565

66-
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
66+
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, int len,
6767
const uint8_t *buf,
68-
unsigned buflen)
68+
int buflen)
6969
{
70-
unsigned int outlen;
70+
int32_t outlen;
7171
/* AVX2 implementation assumes specific buffer lengths */
7272
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN)
7373
{
@@ -83,16 +83,16 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
8383
*/
8484
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
8585
outlen = mld_rej_uniform_eta2_avx2(r, buf);
86-
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
86+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
8787
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
8888
return (int)outlen;
8989
}
9090

91-
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
91+
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, int len,
9292
const uint8_t *buf,
93-
unsigned buflen)
93+
int buflen)
9494
{
95-
unsigned int outlen;
95+
int32_t outlen;
9696
/* AVX2 implementation assumes specific buffer lengths */
9797
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN)
9898
{
@@ -108,7 +108,7 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
108108
*/
109109
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
110110
outlen = mld_rej_uniform_eta4_avx2(r, buf);
111-
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
111+
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * (size_t)outlen);
112112
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
113113
return (int)outlen;
114114
}

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,15 +43,15 @@ void mld_invntt_avx2(__m256i *r, const __m256i *mld_qdata);
4343
void mld_nttunpack_avx2(__m256i *r);
4444

4545
#define mld_rej_uniform_avx2 MLD_NAMESPACE(mld_rej_uniform_avx2)
46-
unsigned mld_rej_uniform_avx2(int32_t *r,
47-
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN]);
46+
int32_t mld_rej_uniform_avx2(int32_t *r,
47+
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN]);
4848

4949
#define mld_rej_uniform_eta2_avx2 MLD_NAMESPACE(mld_rej_uniform_eta2_avx2)
50-
unsigned mld_rej_uniform_eta2_avx2(
50+
int32_t mld_rej_uniform_eta2_avx2(
5151
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN]);
5252

5353
#define mld_rej_uniform_eta4_avx2 MLD_NAMESPACE(mld_rej_uniform_eta4_avx2)
54-
unsigned mld_rej_uniform_eta4_avx2(
54+
int32_t mld_rej_uniform_eta4_avx2(
5555
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN]);
5656

5757
#define mld_poly_decompose_32_avx2 MLD_NAMESPACE(mld_poly_decompose_32_avx2)

‎dev/x86_64/src/rej_uniform_avx2.c‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,8 @@
3636
* frontend to perform the unintuitive padding.
3737
*/
3838

39-
unsigned int mld_rej_uniform_avx2(
40-
int32_t *MLD_RESTRICT r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN])
39+
int32_t mld_rej_uniform_avx2(int32_t *MLD_RESTRICT r,
40+
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN])
4141
{
4242
unsigned int ctr, pos;
4343
uint32_t good;
@@ -116,7 +116,7 @@ unsigned int mld_rej_uniform_avx2(
116116
}
117117
}
118118

119-
return ctr;
119+
return (int32_t)ctr;
120120
}
121121

122122
#else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \

‎dev/x86_64/src/rej_uniform_eta2_avx2.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@
3535
* rej_eta_avx and supports multiple values for ETA via preprocessor
3636
* conditionals. We move the conditionals to the frontend.
3737
*/
38-
unsigned int mld_rej_uniform_eta2_avx2(
38+
int32_t mld_rej_uniform_eta2_avx2(
3939
int32_t *MLD_RESTRICT r,
4040
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN])
4141
{
@@ -139,7 +139,7 @@ unsigned int mld_rej_uniform_eta2_avx2(
139139
}
140140
}
141141

142-
return ctr;
142+
return (int32_t)ctr;
143143
}
144144

145145
#else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \

‎dev/x86_64/src/rej_uniform_eta4_avx2.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@
3636
* conditionals. We move the conditionals to the frontend.
3737
*/
3838

39-
unsigned int mld_rej_uniform_eta4_avx2(
39+
int32_t mld_rej_uniform_eta4_avx2(
4040
int32_t *MLD_RESTRICT r,
4141
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN])
4242
{
@@ -123,7 +123,7 @@ unsigned int mld_rej_uniform_eta4_avx2(
123123
}
124124
}
125125

126-
return ctr;
126+
return (int32_t)ctr;
127127
}
128128

129129
#else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \

‎mldsa/src/cbmc.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -93,14 +93,14 @@
9393
#define forall(qvar, qvar_lb, qvar_ub, predicate) \
9494
__CPROVER_forall \
9595
{ \
96-
unsigned qvar; \
96+
signed int qvar; \
9797
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \
9898
}
9999

100100
#define exists(qvar, qvar_lb, qvar_ub, predicate) \
101101
__CPROVER_exists \
102102
{ \
103-
unsigned qvar; \
103+
signed int qvar; \
104104
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \
105105
}
106106
/* clang-format on */
@@ -119,7 +119,7 @@
119119
value_lb, value_ub) \
120120
__CPROVER_forall \
121121
{ \
122-
unsigned qvar; \
122+
signed int qvar; \
123123
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
124124
(((int)(value_lb) <= ((array_var)[(qvar)])) && \
125125
(((array_var)[(qvar)]) < (int)(value_ub))) \

‎mldsa/src/debug.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,11 @@ void mld_debug_check_assert(const char *file, int line, const int val)
3030
}
3131

3232
void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
33-
unsigned len, int64_t lower_bound_exclusive,
33+
int len, int64_t lower_bound_exclusive,
3434
int64_t upper_bound_exclusive)
3535
{
3636
int err = 0;
37-
unsigned i;
37+
int i;
3838
for (i = 0; i < len; i++)
3939
{
4040
int32_t val = ptr[i];

‎mldsa/src/debug.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ void mld_debug_check_assert(const char *file, int line, const int val);
4343
**************************************************/
4444
#define mld_debug_check_bounds MLD_NAMESPACE(mldsa_debug_check_bounds)
4545
void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
46-
unsigned len, int64_t lower_bound_exclusive,
46+
int len, int64_t lower_bound_exclusive,
4747
int64_t upper_bound_exclusive);
4848

4949
/* Check assertion, calling exit() upon failure

0 commit comments

Comments
 (0)