Skip to content

Commit c707054

Browse files
hanno-beckermkannwischer
hanno-becker
authored and
mkannwischer
committed
Switch mld_polymat to struct wrapper
- Change mld_polymat from mld_polyvecl[MLDSA_K] to struct wrapper - Update all function signatures to use pointer style - Fix all implementations to use struct member access - Update CBMC harnesses and contracts Addresses #737 (step 1 of #736) Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 0e242f8 commit c707054

File tree

11 files changed

+95
-80
lines changed

11 files changed

+95
-80
lines changed

‎mldsa/mldsa_native.S‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -259,6 +259,7 @@
259259
#undef mld_polyz_unpack
260260
/* mldsa/src/polyvec.h */
261261
#undef MLD_POLYVEC_H
262+
#undef mld_polymat
262263
#undef mld_polyvec_matrix_expand
263264
#undef mld_polyvec_matrix_pointwise_montgomery
264265
#undef mld_polyveck

‎mldsa/mldsa_native.c‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,7 @@
256256
#undef mld_polyz_unpack
257257
/* mldsa/src/polyvec.h */
258258
#undef MLD_POLYVEC_H
259+
#undef mld_polymat
259260
#undef mld_polyvec_matrix_expand
260261
#undef mld_polyvec_matrix_pointwise_montgomery
261262
#undef mld_polyveck

‎mldsa/src/polyvec.c‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -31,18 +31,18 @@
3131
* of coefficients.
3232
* No-op unless a native backend with a custom ordering is used.
3333
*/
34-
static void mld_polymat_permute_bitrev_to_custom(mld_polyvecl mat[MLDSA_K])
34+
static void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat)
3535
__contract__(
3636
/* We don't specify that this should be a permutation, but only
3737
* that it does not change the bound established at the end of
3838
* mld_polyvec_matrix_expand.
3939
*/
40-
requires(memory_no_alias(mat, MLDSA_K * sizeof(mld_polyvecl)))
40+
requires(memory_no_alias(mat, sizeof(mld_polymat)))
4141
requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
42-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
43-
assigns(memory_slice(mat, sizeof(mld_polyvecl)*MLDSA_K))
42+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
43+
assigns(memory_slice(mat, sizeof(mld_polymat)))
4444
ensures(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
45-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
45+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
4646
)
4747
{
4848
#if defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER)
@@ -52,7 +52,7 @@ __contract__(
5252
{
5353
for (j = 0; j < MLDSA_L; j++)
5454
{
55-
mld_poly_permute_bitrev_to_custom(mat[i].vec[j].coeffs);
55+
mld_poly_permute_bitrev_to_custom(mat->vec[i].vec[j].coeffs);
5656
}
5757
}
5858

@@ -66,7 +66,7 @@ __contract__(
6666

6767

6868
MLD_INTERNAL_API
69-
void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
69+
void mld_polyvec_matrix_expand(mld_polymat *mat,
7070
const uint8_t rho[MLDSA_SEEDBYTES])
7171
{
7272
unsigned int i, j;
@@ -91,14 +91,14 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
9191
/* Sample 4 matrix entries a time. */
9292
for (i = 0; i < (MLDSA_K * MLDSA_L / 4) * 4; i += 4)
9393
__loop__(
94-
assigns(i, j, object_whole(seed_ext), memory_slice(mat, MLDSA_K * sizeof(mld_polyvecl)))
94+
assigns(i, j, object_whole(seed_ext), memory_slice(mat, sizeof(mld_polymat)))
9595
invariant(i <= (MLDSA_K * MLDSA_L / 4) * 4 && i % 4 == 0)
9696
/* vectors 0 .. i / MLDSA_L are completely sampled */
9797
invariant(forall(k1, 0, i / MLDSA_L, forall(l1, 0, MLDSA_L,
98-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
98+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
9999
/* last vector is sampled up to i % MLDSA_L */
100100
invariant(forall(k2, i / MLDSA_L, i / MLDSA_L + 1, forall(l2, 0, i % MLDSA_L,
101-
array_bound(mat[k2].vec[l2].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
101+
array_bound(mat->vec[k2].vec[l2].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
102102
)
103103
{
104104
for (j = 0; j < 4; j++)
@@ -114,10 +114,10 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
114114
seed_ext[j][MLDSA_SEEDBYTES + 1] = x;
115115
}
116116

117-
mld_poly_uniform_4x(&mat[i / MLDSA_L].vec[i % MLDSA_L],
118-
&mat[(i + 1) / MLDSA_L].vec[(i + 1) % MLDSA_L],
119-
&mat[(i + 2) / MLDSA_L].vec[(i + 2) % MLDSA_L],
120-
&mat[(i + 3) / MLDSA_L].vec[(i + 3) % MLDSA_L],
117+
mld_poly_uniform_4x(&mat->vec[i / MLDSA_L].vec[i % MLDSA_L],
118+
&mat->vec[(i + 1) / MLDSA_L].vec[(i + 1) % MLDSA_L],
119+
&mat->vec[(i + 2) / MLDSA_L].vec[(i + 2) % MLDSA_L],
120+
&mat->vec[(i + 3) / MLDSA_L].vec[(i + 3) % MLDSA_L],
121121
seed_ext);
122122
}
123123
#else /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
@@ -127,19 +127,19 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
127127
/* Entries omitted by the batch-sampling are sampled individually. */
128128
while (i < MLDSA_K * MLDSA_L)
129129
__loop__(
130-
assigns(i, object_whole(seed_ext), memory_slice(mat, MLDSA_K * sizeof(mld_polyvecl)))
130+
assigns(i, object_whole(seed_ext), memory_slice(mat, sizeof(mld_polymat)))
131131
invariant(i <= MLDSA_K * MLDSA_L)
132132
/* vectors 0 .. i / MLDSA_L are completely sampled */
133133
invariant(forall(k1, 0, i / MLDSA_L, forall(l1, 0, MLDSA_L,
134-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
134+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
135135
/* last vector is sampled up to i % MLDSA_L */
136136
invariant(forall(k2, i / MLDSA_L, i / MLDSA_L + 1, forall(l2, 0, i % MLDSA_L,
137-
array_bound(mat[k2].vec[l2].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
137+
array_bound(mat->vec[k2].vec[l2].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
138138
)
139139
{
140140
uint8_t x = (uint8_t)(i / MLDSA_L);
141141
uint8_t y = (uint8_t)(i % MLDSA_L);
142-
mld_poly *this_poly = &mat[i / MLDSA_L].vec[i % MLDSA_L];
142+
mld_poly *this_poly = &mat->vec[i / MLDSA_L].vec[i % MLDSA_L];
143143

144144
seed_ext[0][MLDSA_SEEDBYTES + 0] = y;
145145
seed_ext[0][MLDSA_SEEDBYTES + 1] = x;
@@ -156,7 +156,7 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
156156

157157
MLD_INTERNAL_API
158158
void mld_polyvec_matrix_pointwise_montgomery(mld_polyveck *t,
159-
const mld_polyvecl mat[MLDSA_K],
159+
const mld_polymat *mat,
160160
const mld_polyvecl *v)
161161
{
162162
unsigned int i;
@@ -170,7 +170,7 @@ void mld_polyvec_matrix_pointwise_montgomery(mld_polyveck *t,
170170
array_abs_bound(t->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q)))
171171
)
172172
{
173-
mld_polyvecl_pointwise_acc_montgomery(&t->vec[i], &mat[i], v);
173+
mld_polyvecl_pointwise_acc_montgomery(&t->vec[i], &mat->vec[i], v);
174174
}
175175

176176
mld_assert_abs_bound_2d(t->vec, MLDSA_K, MLDSA_N, MLDSA_Q);

‎mldsa/src/polyvec.h‎

Lines changed: 16 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
* within a single compilation unit. */
1818
#define mld_polyvecl MLD_ADD_PARAM_SET(mld_polyvecl)
1919
#define mld_polyveck MLD_ADD_PARAM_SET(mld_polyveck)
20+
#define mld_polymat MLD_ADD_PARAM_SET(mld_polymat)
2021
/* End of parameter set namespacing */
2122

2223
/* Vectors of polynomials of length MLDSA_L */
@@ -231,6 +232,12 @@ typedef struct
231232
mld_poly vec[MLDSA_K];
232233
} mld_polyveck;
233234

235+
/* Matrix of polynomials (K x L) */
236+
typedef struct
237+
{
238+
mld_polyvecl vec[MLDSA_K];
239+
} mld_polymat;
240+
234241
#define mld_polyveck_reduce MLD_NAMESPACE_KL(polyveck_reduce)
235242
/*************************************************
236243
* Name: polyveck_reduce
@@ -746,18 +753,18 @@ __contract__(
746753
* random coefficients a_{i,j} by performing rejection
747754
* sampling on the output stream of SHAKE128(rho|j|i)
748755
*
749-
* Arguments: - mld_polyvecl mat[MLDSA_K]: output matrix
756+
* Arguments: - mld_polymat *mat: pointer to output matrix
750757
* - const uint8_t rho[]: byte array containing seed rho
751758
**************************************************/
752759
MLD_INTERNAL_API
753-
void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
760+
void mld_polyvec_matrix_expand(mld_polymat *mat,
754761
const uint8_t rho[MLDSA_SEEDBYTES])
755762
__contract__(
756-
requires(memory_no_alias(mat, MLDSA_K * sizeof(mld_polyvecl)))
763+
requires(memory_no_alias(mat, sizeof(mld_polymat)))
757764
requires(memory_no_alias(rho, MLDSA_SEEDBYTES))
758-
assigns(memory_slice(mat, MLDSA_K * sizeof(mld_polyvecl)))
765+
assigns(memory_slice(mat, sizeof(mld_polymat)))
759766
ensures(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
760-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
767+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
761768
);
762769

763770

@@ -780,19 +787,19 @@ __contract__(
780787
* inclusive.
781788
*
782789
* Arguments: - mld_polyveck *t: pointer to output vector t
783-
* - const mld_polyvecl mat[MLDSA_K]: pointer to input matrix
790+
* - const mld_polymat *mat: pointer to input matrix
784791
* - const mld_polyvecl *v: pointer to input vector v
785792
**************************************************/
786793
MLD_INTERNAL_API
787794
void mld_polyvec_matrix_pointwise_montgomery(mld_polyveck *t,
788-
const mld_polyvecl mat[MLDSA_K],
795+
const mld_polymat *mat,
789796
const mld_polyvecl *v)
790797
__contract__(
791798
requires(memory_no_alias(t, sizeof(mld_polyveck)))
792-
requires(memory_no_alias(mat, MLDSA_K*sizeof(mld_polyvecl)))
799+
requires(memory_no_alias(mat, sizeof(mld_polymat)))
793800
requires(memory_no_alias(v, sizeof(mld_polyvecl)))
794801
requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
795-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
802+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
796803
requires(forall(l1, 0, MLDSA_L,
797804
array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
798805
assigns(memory_slice(t, sizeof(mld_polyveck)))

‎mldsa/src/sign.c‎

Lines changed: 21 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -215,16 +215,17 @@ __contract__(
215215
ensures(forall(k2, 0, MLDSA_K, array_bound(t1->vec[k2].coeffs, 0, MLDSA_N, 0, 1 << 10)))
216216
)
217217
{
218-
mld_polyvecl mat[MLDSA_K], s1hat;
218+
mld_polymat mat;
219+
mld_polyvecl s1hat;
219220
mld_polyveck t;
220221

221222
/* Expand matrix */
222-
mld_polyvec_matrix_expand(mat, rho);
223+
mld_polyvec_matrix_expand(&mat, rho);
223224

224225
/* Matrix-vector multiplication */
225226
s1hat = *s1;
226227
mld_polyvecl_ntt(&s1hat);
227-
mld_polyvec_matrix_pointwise_montgomery(&t, mat, &s1hat);
228+
mld_polyvec_matrix_pointwise_montgomery(&t, &mat, &s1hat);
228229
mld_polyveck_reduce(&t);
229230
mld_polyveck_invntt_tomont(&t);
230231

@@ -251,7 +252,7 @@ __contract__(
251252
mld_shake256(tr, MLDSA_TRBYTES, pk, CRYPTO_PUBLICKEYBYTES);
252253

253254
/* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
254-
mld_zeroize(mat, sizeof(mat));
255+
mld_zeroize(&mat, sizeof(mat));
255256
mld_zeroize(&s1hat, sizeof(s1hat));
256257
mld_zeroize(&t, sizeof(t));
257258
}
@@ -407,7 +408,7 @@ __contract__(
407408
* of exactly MLDSA_CRHBYTES bytes
408409
* - const uint8_t *rhoprime: pointer to randomness seed
409410
* - uint16_t nonce: current nonce value
410-
* - const polyvecl mat[MLDSA_K]: expanded matrix
411+
* - const mld_polymat *mat: expanded matrix
411412
* - const polyvecl *s1: secret vector s1
412413
* - const polyveck *s2: secret vector s2
413414
* - const polyveck *t0: vector t0
@@ -423,19 +424,19 @@ MLD_MUST_CHECK_RETURN_VALUE
423424
static int mld_attempt_signature_generation(
424425
uint8_t sig[CRYPTO_BYTES], const uint8_t *mu,
425426
const uint8_t rhoprime[MLDSA_CRHBYTES], uint16_t nonce,
426-
const mld_polyvecl mat[MLDSA_K], const mld_polyvecl *s1,
427-
const mld_polyveck *s2, const mld_polyveck *t0)
427+
const mld_polymat *mat, const mld_polyvecl *s1, const mld_polyveck *s2,
428+
const mld_polyveck *t0)
428429
__contract__(
429430
requires(memory_no_alias(sig, CRYPTO_BYTES))
430431
requires(memory_no_alias(mu, MLDSA_CRHBYTES))
431432
requires(memory_no_alias(rhoprime, MLDSA_CRHBYTES))
432-
requires(memory_no_alias(mat, MLDSA_K * sizeof(mld_polyvecl)))
433+
requires(memory_no_alias(mat, sizeof(mld_polymat)))
433434
requires(memory_no_alias(s1, sizeof(mld_polyvecl)))
434435
requires(memory_no_alias(s2, sizeof(mld_polyveck)))
435436
requires(memory_no_alias(t0, sizeof(mld_polyveck)))
436437
requires(nonce <= NONCE_UB)
437438
requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
438-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
439+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
439440
requires(forall(k2, 0, MLDSA_K, array_abs_bound(t0->vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
440441
requires(forall(k3, 0, MLDSA_L, array_abs_bound(s1->vec[k3].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
441442
requires(forall(k4, 0, MLDSA_K, array_abs_bound(s2->vec[k4].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
@@ -584,7 +585,8 @@ int crypto_sign_signature_internal(uint8_t sig[CRYPTO_BYTES], size_t *siglen,
584585
MLD_ALIGN uint8_t
585586
seedbuf[2 * MLDSA_SEEDBYTES + MLDSA_TRBYTES + 2 * MLDSA_CRHBYTES];
586587
uint8_t *rho, *tr, *key, *mu, *rhoprime;
587-
mld_polyvecl mat[MLDSA_K], s1;
588+
mld_polymat mat;
589+
mld_polyvecl s1;
588590
mld_polyveck t0, s2;
589591

590592
uint16_t nonce = 0;
@@ -614,7 +616,7 @@ int crypto_sign_signature_internal(uint8_t sig[CRYPTO_BYTES], size_t *siglen,
614616
/* Constant time: rho is part of the public key and, hence, public. */
615617
MLD_CT_TESTING_DECLASSIFY(rho, MLDSA_SEEDBYTES);
616618
/* Expand matrix and transform vectors */
617-
mld_polyvec_matrix_expand(mat, rho);
619+
mld_polyvec_matrix_expand(&mat, rho);
618620
mld_polyvecl_ntt(&s1);
619621
mld_polyveck_ntt(&s2);
620622
mld_polyveck_ntt(&t0);
@@ -638,7 +640,7 @@ int crypto_sign_signature_internal(uint8_t sig[CRYPTO_BYTES], size_t *siglen,
638640
/* loop. We can therefore re-assert their bounds here as part of the */
639641
/* loop invariant. This makes proof noticeably faster with CBMC */
640642
invariant(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
641-
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
643+
array_bound(mat.vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
642644
invariant(forall(k2, 0, MLDSA_K, array_abs_bound(t0.vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
643645
invariant(forall(k3, 0, MLDSA_L, array_abs_bound(s1.vec[k3].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
644646
invariant(forall(k4, 0, MLDSA_K, array_abs_bound(s2.vec[k4].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
@@ -661,7 +663,7 @@ int crypto_sign_signature_internal(uint8_t sig[CRYPTO_BYTES], size_t *siglen,
661663
}
662664

663665
attempt_result = mld_attempt_signature_generation(sig, mu, rhoprime, nonce,
664-
mat, &s1, &s2, &t0);
666+
&mat, &s1, &s2, &t0);
665667
nonce++;
666668
if (attempt_result == 0)
667669
{
@@ -673,7 +675,7 @@ int crypto_sign_signature_internal(uint8_t sig[CRYPTO_BYTES], size_t *siglen,
673675

674676
/* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
675677
mld_zeroize(seedbuf, sizeof(seedbuf));
676-
mld_zeroize(mat, sizeof(mat));
678+
mld_zeroize(&mat, sizeof(mat));
677679
mld_zeroize(&s1, sizeof(s1));
678680
mld_zeroize(&s2, sizeof(s2));
679681
mld_zeroize(&t0, sizeof(t0));
@@ -788,7 +790,8 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
788790
MLD_ALIGN uint8_t c[MLDSA_CTILDEBYTES];
789791
MLD_ALIGN uint8_t c2[MLDSA_CTILDEBYTES];
790792
mld_poly cp;
791-
mld_polyvecl mat[MLDSA_K], z;
793+
mld_polymat mat;
794+
mld_polyvecl z;
792795
mld_polyveck t1, w1, tmp, h;
793796

794797
if (siglen != CRYPTO_BYTES)
@@ -827,10 +830,10 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
827830

828831
/* Matrix-vector multiplication; compute Az - c2^dt1 */
829832
mld_poly_challenge(&cp, c);
830-
mld_polyvec_matrix_expand(mat, rho);
833+
mld_polyvec_matrix_expand(&mat, rho);
831834

832835
mld_polyvecl_ntt(&z);
833-
mld_polyvec_matrix_pointwise_montgomery(&w1, mat, &z);
836+
mld_polyvec_matrix_pointwise_montgomery(&w1, &mat, &z);
834837

835838
mld_poly_ntt(&cp);
836839
mld_polyveck_shiftl(&t1);
@@ -881,7 +884,7 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
881884
mld_zeroize(c, sizeof(c));
882885
mld_zeroize(c2, sizeof(c2));
883886
mld_zeroize(&cp, sizeof(cp));
884-
mld_zeroize(mat, sizeof(mat));
887+
mld_zeroize(&mat, sizeof(mat));
885888
mld_zeroize(&z, sizeof(z));
886889
mld_zeroize(&t1, sizeof(t1));
887890
mld_zeroize(&w1, sizeof(w1));

‎proofs/cbmc/attempt_signature_generation/attempt_signature_generation_harness.c‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,18 +3,20 @@
33

44
#include "sign.h"
55

6-
int mld_attempt_signature_generation(
7-
uint8_t *sig, const uint8_t *mu, const uint8_t rhoprime[MLDSA_CRHBYTES],
8-
uint16_t nonce, const mld_polyvecl mat[MLDSA_K], const mld_polyvecl *s1,
9-
const mld_polyveck *s2, const mld_polyveck *t0);
6+
int mld_attempt_signature_generation(uint8_t *sig, const uint8_t *mu,
7+
const uint8_t rhoprime[MLDSA_CRHBYTES],
8+
uint16_t nonce, mld_polymat *mat,
9+
const mld_polyvecl *s1,
10+
const mld_polyveck *s2,
11+
const mld_polyveck *t0);
1012

1113
void harness(void)
1214
{
1315
uint8_t *sig;
1416
uint8_t *mu;
1517
uint8_t *rhoprime;
1618
uint16_t nonce;
17-
mld_polyvecl *mat;
19+
mld_polymat *mat;
1820
mld_polyvecl *s1;
1921
mld_polyveck *s2;
2022
mld_polyveck *t0;

‎proofs/cbmc/polymat_permute_bitrev_to_custom/polymat_permute_bitrev_to_custom_harness.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@
33

44
#include "polyvec.h"
55

6-
void mld_polymat_permute_bitrev_to_custom(mld_polyvecl mat[MLDSA_K]);
6+
void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat);
77

88
void harness(void)
99
{
10-
mld_polyvecl *mat;
10+
mld_polymat *mat;
1111
mld_polymat_permute_bitrev_to_custom(mat);
1212
}

‎proofs/cbmc/polyvec_matrix_expand/polyvec_matrix_expand_harness.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
void harness(void)
77
{
8-
mld_polyvecl *mat;
8+
mld_polymat *mat;
99
uint8_t *rho;
1010

1111
mld_polyvec_matrix_expand(mat, rho);

‎proofs/cbmc/polyvec_matrix_expand_serial/polyvec_matrix_expand_harness.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
void harness(void)
77
{
8-
mld_polyvecl *mat;
8+
mld_polymat *mat;
99
uint8_t *rho;
1010

1111
mld_polyvec_matrix_expand(mat, rho);

0 commit comments

Comments
 (0)