Skip to content

Commit 2326617

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 257e8f8 commit 2326617

Some content is hidden

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

55 files changed

+462
-463
lines changed

‎dev/aarch64_clean/meta.h‎

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -46,24 +46,23 @@ static MLD_INLINE void mld_intt_native(int32_t data[MLDSA_N])
4646
mld_aarch64_intt_zetas_layer123456);
4747
}
4848

49-
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
50-
const uint8_t *buf,
51-
unsigned buflen)
49+
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, int len,
50+
const uint8_t *buf, int buflen)
5251
{
5352
if (len != MLDSA_N || buflen % 24 != 0)
5453
{
5554
return -1;
5655
}
5756

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

62-
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
61+
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, int len,
6362
const uint8_t *buf,
64-
unsigned buflen)
63+
int buflen)
6564
{
66-
unsigned int outlen;
65+
int32_t outlen;
6766
/* AArch64 implementation assumes specific buffer lengths */
6867
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
6968
{
@@ -83,11 +82,11 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
8382
return (int)outlen;
8483
}
8584

86-
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
85+
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, int len,
8786
const uint8_t *buf,
88-
unsigned buflen)
87+
int buflen)
8988
{
90-
unsigned int outlen;
89+
int32_t outlen;
9190
/* AArch64 implementation assumes specific buffer lengths */
9291
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
9392
{

‎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: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -49,9 +49,8 @@ static MLD_INLINE void mld_intt_native(int32_t data[MLDSA_N])
4949
mld_invntt_avx2((__m256i *)data, mld_qdata.vec);
5050
}
5151

52-
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
53-
const uint8_t *buf,
54-
unsigned buflen)
52+
static MLD_INLINE int mld_rej_uniform_native(int32_t *r, int len,
53+
const uint8_t *buf, int buflen)
5554
{
5655
/* AVX2 implementation assumes specific buffer lengths */
5756
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_BUFLEN)
@@ -63,11 +62,11 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
6362
return (int)mld_rej_uniform_avx2(r, buf);
6463
}
6564

66-
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
65+
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, int len,
6766
const uint8_t *buf,
68-
unsigned buflen)
67+
int buflen)
6968
{
70-
unsigned int outlen;
69+
int32_t outlen;
7170
/* AVX2 implementation assumes specific buffer lengths */
7271
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN)
7372
{
@@ -88,11 +87,11 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
8887
return (int)outlen;
8988
}
9089

91-
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
90+
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, int len,
9291
const uint8_t *buf,
93-
unsigned buflen)
92+
int buflen)
9493
{
95-
unsigned int outlen;
94+
int32_t outlen;
9695
/* AVX2 implementation assumes specific buffer lengths */
9796
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN)
9897
{

‎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: 7 additions & 7 deletions
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
@@ -91,14 +91,14 @@ void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
9191

9292
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
9393
* just use a single flattened array_bound(...) here. */
94-
#define mld_assert_bound_2d(ptr, M, N, value_lb, value_ub) \
95-
cassert(forall(kN, 0, (M), \
96-
array_bound(&((int32_t(*)[(N)])(ptr))[kN][0], 0, (N), \
94+
#define mld_assert_bound_2d(ptr, M, N, value_lb, value_ub) \
95+
cassert(forall(kN, 0, (M), \
96+
array_bound(&((int32_t (*)[(N)])(ptr))[kN][0], 0, (N), \
9797
(value_lb), (value_ub))))
9898

99-
#define mld_assert_abs_bound_2d(ptr, M, N, value_abs_bd) \
100-
cassert(forall(kN, 0, (M), \
101-
array_abs_bound(&((int32_t(*)[(N)])(ptr))[kN][0], 0, (N), \
99+
#define mld_assert_abs_bound_2d(ptr, M, N, value_abs_bd) \
100+
cassert(forall(kN, 0, (M), \
101+
array_abs_bound(&((int32_t (*)[(N)])(ptr))[kN][0], 0, (N), \
102102
(value_abs_bd))))
103103

104104
#else /* !MLDSA_DEBUG && CBMC */

0 commit comments

Comments
 (0)