Skip to content

Commit 7c4ed09

Browse files
hanno-beckerhanno-becker
committed
[WIP] Reduce visual clutter in CBMC specs
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 0749d2d commit 7c4ed09

File tree

23 files changed

+515
-598
lines changed

23 files changed

+515
-598
lines changed

‎dev/fips202/aarch64/src/fips202_native_aarch64.h‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -18,45 +18,45 @@ extern const uint64_t mld_keccakf1600_round_constants[];
1818
#define mld_keccak_f1600_x1_scalar_asm MLD_NAMESPACE(keccak_f1600_x1_scalar_asm)
1919
void mld_keccak_f1600_x1_scalar_asm(uint64_t *state, uint64_t const *rc)
2020
__contract__(
21-
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
21+
requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 1))
2222
requires(rc == mld_keccakf1600_round_constants)
23-
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
23+
assigns_slices(state, sizeof(uint64_t) * 25 * 1)
2424
);
2525

2626
#define mld_keccak_f1600_x1_v84a_asm MLD_NAMESPACE(keccak_f1600_x1_v84a_asm)
2727
void mld_keccak_f1600_x1_v84a_asm(uint64_t *state, uint64_t const *rc)
2828
__contract__(
29-
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
29+
requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 1))
3030
requires(rc == mld_keccakf1600_round_constants)
31-
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
31+
assigns_slices(state, sizeof(uint64_t) * 25 * 1)
3232
);
3333

3434
#define mld_keccak_f1600_x2_v84a_asm MLD_NAMESPACE(keccak_f1600_x2_v84a_asm)
3535
void mld_keccak_f1600_x2_v84a_asm(uint64_t *state, uint64_t const *rc)
3636
__contract__(
37-
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2))
37+
requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 2))
3838
requires(rc == mld_keccakf1600_round_constants)
39-
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))
39+
assigns_slices(state, sizeof(uint64_t) * 25 * 2)
4040
);
4141

4242
#define mld_keccak_f1600_x4_scalar_v8a_hybrid_asm \
4343
MLD_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
4444
void mld_keccak_f1600_x4_scalar_v8a_hybrid_asm(uint64_t *state,
4545
uint64_t const *rc)
4646
__contract__(
47-
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
47+
requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 4))
4848
requires(rc == mld_keccakf1600_round_constants)
49-
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
49+
assigns_slices(state, sizeof(uint64_t) * 25 * 4)
5050
);
5151

5252
#define mld_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm \
5353
MLD_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm)
5454
void mld_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm(uint64_t *state,
5555
uint64_t const *rc)
5656
__contract__(
57-
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
57+
requires(slices_no_alias(state, sizeof(uint64_t) * 25 * 4))
5858
requires(rc == mld_keccakf1600_round_constants)
59-
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
59+
assigns_slices(state, sizeof(uint64_t) * 25 * 4)
6060
);
6161

6262
#endif /* !MLD_FIPS202_NATIVE_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */

‎mldsa/src/cbmc.h‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,84 @@
108108
/***************************************************
109109
* Convenience macros for common contract patterns
110110
***************************************************/
111+
112+
/* Helper to chain conditions with && */
113+
#define objects_no_alias1(x) memory_no_alias((x), sizeof(*(x)))
114+
#define objects_no_alias2(x, y) (objects_no_alias1(x) && objects_no_alias1(y))
115+
#define objects_no_alias3(x, y, z) \
116+
(objects_no_alias2(x, y) && objects_no_alias1(z))
117+
#define objects_no_alias4(x, y, z, w) \
118+
(objects_no_alias3(x, y, z) && objects_no_alias1(w))
119+
#define objects_no_alias5(x, y, z, w, v) \
120+
(objects_no_alias4(x, y, z, w) && objects_no_alias1(v))
121+
#define objects_no_alias6(x, y, z, w, v, u) \
122+
(objects_no_alias5(x, y, z, w, v) && objects_no_alias1(u))
123+
#define objects_no_alias7(x, y, z, w, v, u, t) \
124+
(objects_no_alias6(x, y, z, w, v, u) && objects_no_alias1(t))
125+
#define objects_no_alias8(x, y, z, w, v, u, t, s) \
126+
(objects_no_alias7(x, y, z, w, v, u, t) && objects_no_alias1(s))
127+
#define objects_no_alias9(x, y, z, w, v, u, t, s, r) \
128+
(objects_no_alias8(x, y, z, w, v, u, t, s) && objects_no_alias1(r))
129+
#define objects_no_alias10(x, y, z, w, v, u, t, s, r, q) \
130+
(objects_no_alias9(x, y, z, w, v, u, t, s, r) && objects_no_alias1(q))
131+
132+
#define select_macro(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10, NAME, ...) NAME
133+
#define objects_no_alias(...) \
134+
select_macro(__VA_ARGS__, objects_no_alias10, objects_no_alias9, \
135+
objects_no_alias8, objects_no_alias7, objects_no_alias6, \
136+
objects_no_alias5, objects_no_alias4, objects_no_alias3, \
137+
objects_no_alias2, objects_no_alias1)(__VA_ARGS__)
138+
139+
#define slices_no_alias1(x, sz) memory_no_alias((x), (sz))
140+
#define slices_no_alias2(x0, sz0, x1, sz1) \
141+
(slices_no_alias1(x0, sz0) && slices_no_alias1(x1, sz1))
142+
#define slices_no_alias3(x0, sz0, x1, sz1, x2, sz2) \
143+
(slices_no_alias2(x0, sz0, x1, sz1) && slices_no_alias1(x2, sz2))
144+
#define slices_no_alias4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) \
145+
(slices_no_alias3(x0, sz0, x1, sz1, x2, sz2) && slices_no_alias1(x3, sz3))
146+
#define slices_no_alias5(x0, sz0, x1, sz1, x2, sz2, x3, sz3, x4, sz4) \
147+
(slices_no_alias4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) && \
148+
slices_no_alias1(x4, sz4))
149+
150+
#define get_arrs_macro(_1, _2, _3, _4, _5, NAME, ...) NAME
151+
#define slices_no_alias(...) \
152+
select_macro(__VA_ARGS__, dummy10, dummy9, dummy8, dummy7, dummy6, \
153+
_SLICES_NO_ALIAS_5, _SLICES_NO_ALIAS_4, _SLICES_NO_ALIAS_3, \
154+
_SLICES_NO_ALIAS_2, _SLICES_NO_ALIAS_1)(__VA_ARGS__)
155+
156+
/* Helper to chain assigns clauses */
157+
#define assigns_objs1(x) assigns(memory_slice((x), sizeof(*(x))))
158+
#define assigns_objs2(x, y) assigns_objs1(x) assigns_objs1(y)
159+
#define assigns_objs3(x, y, z) assigns_objs2(x, y) assigns_objs1(z)
160+
#define assigns_objs4(x, y, z, w) assigns_objs3(x, y, z) assigns_objs1(w)
161+
#define assigns_objs5(x, y, z, w, v) assigns_objs4(x, y, z, w) assigns_objs1(v)
162+
#define assigns_objs6(x, y, z, w, v, u) \
163+
assigns_objs5(x, y, z, w, v) assigns_objs1(u)
164+
#define assigns_objs7(x, y, z, w, v, u, t) \
165+
assigns_objs6(x, y, z, w, v, u) assigns_objs1(t)
166+
#define assigns_objs8(x, y, z, w, v, u, t, s) \
167+
assigns_objs7(x, y, z, w, v, u, t) assigns_objs1(s)
168+
169+
#define assigns_objs(...) \
170+
select_macro(__VA_ARGS__, dummy10, dummy9, _assigns_objs8, _assigns_objs7, \
171+
_assigns_objs6, _assigns_objs5, _assigns_objs4, _assigns_objs3, \
172+
_assigns_objs2, _assigns_objs1)(__VA_ARGS__)
173+
174+
#define assigns_slices1(x, sz) assigns(memory_slice((x), (sz)))
175+
#define assigns_slices2(x0, sz0, x1, sz1) \
176+
assigns_slices1(x0, sz0) assigns_slices1(x1, sz1)
177+
#define assigns_slices3(x0, sz0, x1, sz1, x2, sz2) \
178+
assigns_slices2(x0, sz0, x1, sz1) assigns_slices1(x2, sz2)
179+
#define assigns_slices4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) \
180+
assigns_slices3(x0, sz0, x1, sz1, x2, sz2) assigns_slices1(x3, sz3)
181+
#define assigns_slices5(x0, sz0, x1, sz1, x2, sz2, x3, sz3, x4, sz4) \
182+
assigns_slices4(x0, sz0, x1, sz1, x2, sz2, x3, sz3) assigns_slices1(x4, sz4)
183+
184+
#define assigns_slices(...) \
185+
select_macro(__VA_ARGS__, dummy10, dummy9, dummy8, dummy7, dummy6, \
186+
assigns_slices5, assigns_slices4, assigns_slices3, \
187+
assigns_slices2, assigns_slices1)(__VA_ARGS__)
188+
111189
/*
112190
* Prevent clang-format from corrupting CBMC's special ==> operator
113191
*/

‎mldsa/src/ct.h‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -268,8 +268,7 @@ static MLD_INLINE uint8_t mld_ct_memcmp(const void *a, const void *b,
268268
const size_t len)
269269
__contract__(
270270
requires(len <= UINT16_MAX)
271-
requires(memory_no_alias(a, len))
272-
requires(memory_no_alias(b, len))
271+
requires(slices_no_alias(a, len, b, len))
273272
ensures((return_value == 0) == forall(i, 0, len, (((const uint8_t *)a)[i] == ((const uint8_t *)b)[i])))
274273
)
275274
{
@@ -307,8 +306,8 @@ __contract__(
307306
**************************************************/
308307
static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
309308
__contract__(
310-
requires(memory_no_alias(ptr, len))
311-
assigns(memory_slice(ptr, len))
309+
requires(slices_no_alias(ptr, len))
310+
assigns_slices(ptr, len)
312311
);
313312

314313
#if defined(MLD_CONFIG_CUSTOM_ZEROIZE)

‎mldsa/src/fips202/fips202.c‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -49,8 +49,8 @@
4949
**************************************************/
5050
static void keccak_init(uint64_t s[MLD_KECCAK_LANES])
5151
__contract__(
52-
requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
53-
assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
52+
requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
53+
assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES)
5454
)
5555
{
5656
mld_memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES);
@@ -76,9 +76,9 @@ __contract__(
7676
requires(inlen <= MLD_MAX_BUFFER_SIZE)
7777
requires(r < sizeof(uint64_t) * MLD_KECCAK_LANES)
7878
requires(pos <= r)
79-
requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
80-
requires(memory_no_alias(in, inlen))
81-
assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
79+
requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES,
80+
in, inlen))
81+
assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES)
8282
ensures(return_value < r))
8383
{
8484
while (inlen >= r - pos)
@@ -118,8 +118,8 @@ static void keccak_finalize(uint64_t s[MLD_KECCAK_LANES], unsigned int pos,
118118
__contract__(
119119
requires(pos <= r && r < sizeof(uint64_t) * MLD_KECCAK_LANES)
120120
requires((r / 8) >= 1)
121-
requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
122-
assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
121+
requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
122+
assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES)
123123
)
124124
{
125125
uint8_t b = 0x80;
@@ -151,10 +151,10 @@ __contract__(
151151
(r == SHAKE256_RATE && pos <= SHAKE256_RATE) ||
152152
(r == SHA3_512_RATE && pos <= SHA3_512_RATE))
153153
requires(outlen <= 8 * r /* somewhat arbitrary bound */)
154-
requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
155-
requires(memory_no_alias(out, outlen))
156-
assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
157-
assigns(memory_slice(out, outlen))
154+
requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES,
155+
out, outlen))
156+
assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES,
157+
out, outlen)
158158
ensures(return_value <= r))
159159
{
160160
unsigned int i;

‎mldsa/src/fips202/fips202.h‎

Lines changed: 28 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -41,8 +41,8 @@ typedef struct
4141
**************************************************/
4242
void mld_shake128_init(mld_shake128ctx *state)
4343
__contract__(
44-
requires(memory_no_alias(state, sizeof(mld_shake128ctx)))
45-
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
44+
requires(objs_no_alias(state))
45+
assigns_objs(state)
4646
ensures(state->pos == 0)
4747
);
4848

@@ -61,10 +61,10 @@ void mld_shake128_absorb(mld_shake128ctx *state, const uint8_t *in,
6161
size_t inlen)
6262
__contract__(
6363
requires(inlen <= MLD_MAX_BUFFER_SIZE)
64-
requires(memory_no_alias(state, sizeof(mld_shake128ctx)))
65-
requires(memory_no_alias(in, inlen))
64+
requires(objs_no_alias(state))
65+
requires(slices_no_alias(in, inlen))
6666
requires(state->pos <= SHAKE128_RATE)
67-
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
67+
assigns_objs(state)
6868
ensures(state->pos <= SHAKE128_RATE)
6969
);
7070

@@ -78,9 +78,9 @@ __contract__(
7878
**************************************************/
7979
void mld_shake128_finalize(mld_shake128ctx *state)
8080
__contract__(
81-
requires(memory_no_alias(state, sizeof(mld_shake128ctx)))
81+
requires(objs_no_alias(state))
8282
requires(state->pos <= SHAKE128_RATE)
83-
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
83+
assigns_objs(state)
8484
ensures(state->pos <= SHAKE128_RATE)
8585
);
8686

@@ -99,11 +99,11 @@ __contract__(
9999
void mld_shake128_squeeze(uint8_t *out, size_t outlen, mld_shake128ctx *state)
100100
__contract__(
101101
requires(outlen <= 8 * SHAKE128_RATE /* somewhat arbitrary bound */)
102-
requires(memory_no_alias(state, sizeof(mld_shake128ctx)))
103-
requires(memory_no_alias(out, outlen))
102+
requires(objs_no_alias(state))
103+
requires(slices_no_alias(out, outlen))
104104
requires(state->pos <= SHAKE128_RATE)
105-
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
106-
assigns(memory_slice(out, outlen))
105+
assigns_objs(state)
106+
assigns_slices(out, outlen)
107107
ensures(state->pos <= SHAKE128_RATE)
108108
);
109109

@@ -117,8 +117,8 @@ __contract__(
117117
**************************************************/
118118
void mld_shake128_release(mld_shake128ctx *state)
119119
__contract__(
120-
requires(memory_no_alias(state, sizeof(mld_shake128ctx)))
121-
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
120+
requires(objs_no_alias(state))
121+
assigns_objs(state)
122122
);
123123

124124
#define mld_shake256_init MLD_NAMESPACE(shake256_init)
@@ -131,8 +131,8 @@ __contract__(
131131
**************************************************/
132132
void mld_shake256_init(mld_shake256ctx *state)
133133
__contract__(
134-
requires(memory_no_alias(state, sizeof(mld_shake256ctx)))
135-
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
134+
requires(objs_no_alias(state))
135+
assigns_objs(state)
136136
ensures(state->pos == 0)
137137
);
138138

@@ -151,10 +151,10 @@ void mld_shake256_absorb(mld_shake256ctx *state, const uint8_t *in,
151151
size_t inlen)
152152
__contract__(
153153
requires(inlen <= MLD_MAX_BUFFER_SIZE)
154-
requires(memory_no_alias(state, sizeof(mld_shake256ctx)))
155-
requires(memory_no_alias(in, inlen))
154+
requires(objs_no_alias(state))
155+
requires(slices_no_alias(in, inlen))
156156
requires(state->pos <= SHAKE256_RATE)
157-
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
157+
assigns_objs(state)
158158
ensures(state->pos <= SHAKE256_RATE)
159159
);
160160

@@ -168,9 +168,9 @@ __contract__(
168168
**************************************************/
169169
void mld_shake256_finalize(mld_shake256ctx *state)
170170
__contract__(
171-
requires(memory_no_alias(state, sizeof(mld_shake256ctx)))
171+
requires(objs_no_alias(state))
172172
requires(state->pos <= SHAKE256_RATE)
173-
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
173+
assigns_objs(state)
174174
ensures(state->pos <= SHAKE256_RATE)
175175
);
176176

@@ -189,11 +189,11 @@ __contract__(
189189
void mld_shake256_squeeze(uint8_t *out, size_t outlen, mld_shake256ctx *state)
190190
__contract__(
191191
requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */)
192-
requires(memory_no_alias(state, sizeof(mld_shake256ctx)))
193-
requires(memory_no_alias(out, outlen))
192+
requires(objs_no_alias(state))
193+
requires(slices_no_alias(out, outlen))
194194
requires(state->pos <= SHAKE256_RATE)
195-
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
196-
assigns(memory_slice(out, outlen))
195+
assigns_objs(state)
196+
assigns_slices(out, outlen)
197197
ensures(state->pos <= SHAKE256_RATE)
198198
);
199199

@@ -207,8 +207,8 @@ __contract__(
207207
**************************************************/
208208
void mld_shake256_release(mld_shake256ctx *state)
209209
__contract__(
210-
requires(memory_no_alias(state, sizeof(mld_shake256ctx)))
211-
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
210+
requires(objs_no_alias(state))
211+
assigns_objs(state)
212212
);
213213

214214
#define mld_shake256 MLD_NAMESPACE(shake256)
@@ -226,9 +226,8 @@ void mld_shake256(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen)
226226
__contract__(
227227
requires(inlen <= MLD_MAX_BUFFER_SIZE)
228228
requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */)
229-
requires(memory_no_alias(in, inlen))
230-
requires(memory_no_alias(out, outlen))
231-
assigns(memory_slice(out, outlen))
229+
requires(slices_no_alias(in, inlen, out, outlen))
230+
assigns_slices(out, outlen)
232231
);
233232

234233
#endif /* !MLD_FIPS202_FIPS202_H */

‎mldsa/src/fips202/fips202x4.c‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -28,13 +28,13 @@ static void mld_keccak_absorb_once_x4(uint64_t *s, uint32_t r,
2828
size_t inlen, uint8_t p)
2929
__contract__(
3030
requires(inlen <= MLD_MAX_BUFFER_SIZE)
31-
requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
3231
requires(r <= sizeof(uint64_t) * MLD_KECCAK_LANES)
33-
requires(memory_no_alias(in0, inlen))
34-
requires(memory_no_alias(in1, inlen))
35-
requires(memory_no_alias(in2, inlen))
36-
requires(memory_no_alias(in3, inlen))
37-
assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)))
32+
requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY,
33+
in0, inlen,
34+
in1, inlen,
35+
in2, inlen,
36+
in3, inlen))
37+
assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
3838
{
3939
while (inlen >= r)
4040
__loop__(
@@ -81,16 +81,16 @@ static void mld_keccak_squeezeblocks_x4(uint8_t *out0, uint8_t *out1,
8181
__contract__(
8282
requires(r <= sizeof(uint64_t) * MLD_KECCAK_LANES)
8383
requires(nblocks <= 8 /* somewhat arbitrary bound */)
84-
requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
85-
requires(memory_no_alias(out0, nblocks * r))
86-
requires(memory_no_alias(out1, nblocks * r))
87-
requires(memory_no_alias(out2, nblocks * r))
88-
requires(memory_no_alias(out3, nblocks * r))
89-
assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
90-
assigns(memory_slice(out0, nblocks * r))
91-
assigns(memory_slice(out1, nblocks * r))
92-
assigns(memory_slice(out2, nblocks * r))
93-
assigns(memory_slice(out3, nblocks * r)))
84+
requires(slices_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY,
85+
out0, nblocks * r,
86+
out1, nblocks * r,
87+
out2, nblocks * r,
88+
out3, nblocks * r))
89+
assigns_slices(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY,
90+
out0, nblocks * r,
91+
out1, nblocks * r,
92+
out2, nblocks * r,
93+
out3, nblocks * r))
9494
{
9595
while (nblocks > 0)
9696
__loop__(

0 commit comments

Comments
 (0)