Skip to content

Commit 71773d9

Browse files
hanno-beckermkannwischer
hanno-becker
authored and
mkannwischer
committed
CBMC: Remove uses of object_whole
In preparation for the introduction of workspace structures at the higher-level APIs, this commit removes all uses of the CBMC footprint predicate `object_whole` and instead uses the more fine-grained `memory_slice`. For `mlk_poly_getnoise_eta1122_4x`, we also remove the sole use of `same_object` in the code base, and remove its definition from cbmc.h. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent ee486b6 commit 71773d9

File tree

16 files changed

+62
-63
lines changed

16 files changed

+62
-63
lines changed

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ __contract__(
9494
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
9595
requires(zetas == mlk_aarch64_zetas_mulcache_native)
9696
requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
97-
assigns(object_whole(cache))
97+
assigns(memory_slice(cache, sizeof(int16_t) * (MLKEM_N / 2)))
9898
ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
9999
);
100100

@@ -106,7 +106,7 @@ __contract__(
106106
requires(memory_no_alias(r, MLKEM_POLYBYTES))
107107
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
108108
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
109-
assigns(object_whole(r))
109+
assigns(memory_slice(r, MLKEM_POLYBYTES))
110110
);
111111

112112
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ __contract__(
9393
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
9494
requires(zetas == mlk_aarch64_zetas_mulcache_native)
9595
requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
96-
assigns(object_whole(cache))
96+
assigns(memory_slice(cache, sizeof(int16_t) * (MLKEM_N / 2)))
9797
ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
9898
);
9999

@@ -105,7 +105,7 @@ __contract__(
105105
requires(memory_no_alias(r, MLKEM_POLYBYTES))
106106
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
107107
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
108-
assigns(object_whole(r))
108+
assigns(memory_slice(r, MLKEM_POLYBYTES))
109109
);
110110

111111
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \

‎mlkem/src/cbmc.h‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,6 @@
5050
*/
5151
#define object_whole(...) __CPROVER_object_whole(__VA_ARGS__)
5252
#define memory_slice(...) __CPROVER_object_upto(__VA_ARGS__)
53-
#define same_object(...) __CPROVER_same_object(__VA_ARGS__)
5453

5554
/*
5655
* Pointer-related predicates

‎mlkem/src/compress.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -457,7 +457,7 @@ __contract__(
457457
requires(memory_no_alias(r, MLKEM_POLYBYTES))
458458
requires(memory_no_alias(a, sizeof(mlk_poly)))
459459
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
460-
assigns(object_whole(r))
460+
assigns(memory_slice(r, MLKEM_POLYBYTES))
461461
)
462462
{
463463
unsigned i;

‎mlkem/src/compress.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -598,7 +598,7 @@ __contract__(
598598
requires(memory_no_alias(r, MLKEM_POLYBYTES))
599599
requires(memory_no_alias(a, sizeof(mlk_poly)))
600600
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
601-
assigns(object_whole(r))
601+
assigns(memory_slice(r, MLKEM_POLYBYTES))
602602
);
603603

604604

@@ -654,7 +654,7 @@ void mlk_poly_frommsg(mlk_poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES])
654654
__contract__(
655655
requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES))
656656
requires(memory_no_alias(r, sizeof(mlk_poly)))
657-
assigns(object_whole(r))
657+
assigns(memory_slice(r, sizeof(mlk_poly)))
658658
ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
659659
);
660660

@@ -683,7 +683,7 @@ __contract__(
683683
requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES))
684684
requires(memory_no_alias(r, sizeof(mlk_poly)))
685685
requires(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
686-
assigns(object_whole(msg))
686+
assigns(memory_slice(msg, MLKEM_INDCPA_MSGBYTES))
687687
);
688688

689689
#endif /* !MLK_COMPRESS_H */

‎mlkem/src/fips202/fips202x4.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ __contract__(
3030
requires(memory_no_alias(in1, inlen))
3131
requires(memory_no_alias(in2, inlen))
3232
requires(memory_no_alias(in3, inlen))
33-
assigns(object_whole(state))
33+
assigns(memory_slice(state, sizeof(mlk_shake128x4ctx)))
3434
);
3535

3636
#define mlk_shake128x4_squeezeblocks MLK_NAMESPACE(shake128x4_squeezeblocks)
@@ -48,7 +48,7 @@ __contract__(
4848
memory_slice(out1, nblocks * SHAKE128_RATE),
4949
memory_slice(out2, nblocks * SHAKE128_RATE),
5050
memory_slice(out3, nblocks * SHAKE128_RATE),
51-
object_whole(state))
51+
memory_slice(state, sizeof(mlk_shake128x4ctx)))
5252
);
5353

5454
#define mlk_shake128x4_init MLK_NAMESPACE(shake128x4_init)

‎mlkem/src/indcpa.c‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -222,14 +222,14 @@ __contract__(
222222
requires(memory_no_alias(a, sizeof(mlk_polymat)))
223223
requires(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
224224
array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
225-
assigns(object_whole(a))
225+
assigns(memory_slice(a, sizeof(mlk_polymat)))
226226
ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
227227
array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
228228
{
229229
unsigned i;
230230
for (i = 0; i < MLKEM_K; i++)
231231
__loop__(
232-
assigns(i, object_whole(a))
232+
assigns(i, memory_slice(a, sizeof(mlk_polymat)))
233233
invariant(i <= MLKEM_K)
234234
invariant(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
235235
array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
@@ -354,12 +354,12 @@ __contract__(
354354
requires(forall(k0, 0, MLKEM_K,
355355
forall(k1, 0, MLKEM_K,
356356
array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))))
357-
assigns(object_whole(out)))
357+
assigns(memory_slice(out, sizeof(mlk_polyvec))))
358358
{
359359
unsigned i;
360360
for (i = 0; i < MLKEM_K; i++)
361361
__loop__(
362-
assigns(i, object_whole(out))
362+
assigns(i, memory_slice(out, sizeof(mlk_polyvec)))
363363
invariant(i <= MLKEM_K))
364364
{
365365
mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc);

‎mlkem/src/indcpa.h‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ __contract__(
4545
requires(memory_no_alias(a, sizeof(mlk_polymat)))
4646
requires(memory_no_alias(seed, MLKEM_SYMBYTES))
4747
requires(transposed == 0 || transposed == 1)
48-
assigns(object_whole(a))
48+
assigns(memory_slice(a, sizeof(mlk_polymat)))
4949
ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
5050
array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
5151
);
@@ -75,8 +75,8 @@ __contract__(
7575
requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
7676
requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES))
7777
requires(memory_no_alias(coins, MLKEM_SYMBYTES))
78-
assigns(object_whole(pk))
79-
assigns(object_whole(sk))
78+
assigns(memory_slice(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
79+
assigns(memory_slice(sk, MLKEM_INDCPA_SECRETKEYBYTES))
8080
);
8181

8282
#define mlk_indcpa_enc MLK_NAMESPACE_K(indcpa_enc)
@@ -109,7 +109,7 @@ __contract__(
109109
requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES))
110110
requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
111111
requires(memory_no_alias(coins, MLKEM_SYMBYTES))
112-
assigns(object_whole(c))
112+
assigns(memory_slice(c, MLKEM_INDCPA_BYTES))
113113
);
114114

115115
#define mlk_indcpa_dec MLK_NAMESPACE_K(indcpa_dec)
@@ -137,7 +137,7 @@ __contract__(
137137
requires(memory_no_alias(c, MLKEM_INDCPA_BYTES))
138138
requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES))
139139
requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES))
140-
assigns(object_whole(m))
140+
assigns(memory_slice(m, MLKEM_INDCPA_MSGBYTES))
141141
);
142142

143143
#endif /* !MLK_INDCPA_H */

‎mlkem/src/kem.h‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -143,8 +143,8 @@ __contract__(
143143
requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
144144
requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
145145
requires(memory_no_alias(coins, 2 * MLKEM_SYMBYTES))
146-
assigns(object_whole(pk))
147-
assigns(object_whole(sk))
146+
assigns(memory_slice(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
147+
assigns(memory_slice(sk, MLKEM_INDCCA_SECRETKEYBYTES))
148148
);
149149

150150
/*************************************************
@@ -173,8 +173,8 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
173173
__contract__(
174174
requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
175175
requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
176-
assigns(object_whole(pk))
177-
assigns(object_whole(sk))
176+
assigns(memory_slice(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
177+
assigns(memory_slice(sk, MLKEM_INDCCA_SECRETKEYBYTES))
178178
);
179179

180180
/*************************************************
@@ -213,8 +213,8 @@ __contract__(
213213
requires(memory_no_alias(ss, MLKEM_SSBYTES))
214214
requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
215215
requires(memory_no_alias(coins, MLKEM_SYMBYTES))
216-
assigns(object_whole(ct))
217-
assigns(object_whole(ss))
216+
assigns(memory_slice(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
217+
assigns(memory_slice(ss, MLKEM_SSBYTES))
218218
);
219219

220220
/*************************************************
@@ -248,8 +248,8 @@ __contract__(
248248
requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
249249
requires(memory_no_alias(ss, MLKEM_SSBYTES))
250250
requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
251-
assigns(object_whole(ct))
252-
assigns(object_whole(ss))
251+
assigns(memory_slice(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
252+
assigns(memory_slice(ss, MLKEM_SSBYTES))
253253
);
254254

255255
/*************************************************
@@ -283,7 +283,7 @@ __contract__(
283283
requires(memory_no_alias(ss, MLKEM_SSBYTES))
284284
requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
285285
requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
286-
assigns(object_whole(ss))
286+
assigns(memory_slice(ss, MLKEM_SSBYTES))
287287
);
288288

289289
#endif /* !MLK_KEM_H */

‎mlkem/src/native/aarch64/src/arith_native_aarch64.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ __contract__(
9393
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
9494
requires(zetas == mlk_aarch64_zetas_mulcache_native)
9595
requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
96-
assigns(object_whole(cache))
96+
assigns(memory_slice(cache, sizeof(int16_t) * (MLKEM_N / 2)))
9797
ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
9898
);
9999

@@ -105,7 +105,7 @@ __contract__(
105105
requires(memory_no_alias(r, MLKEM_POLYBYTES))
106106
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
107107
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
108-
assigns(object_whole(r))
108+
assigns(memory_slice(r, MLKEM_POLYBYTES))
109109
);
110110

111111
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \

0 commit comments

Comments
 (0)