Skip to content

Commit 346d59e

Browse files
mkannwischerhanno-becker
mkannwischer
authored and
hanno-becker
committed
CBMC: Replace object_whole with memory_slice in non-top-level contracts
This commit replaces object_whole with memory_slice in all non-top-level contracts in preparation of #713 Top-level contracts are unchanged. Note also that object_whole is still used in loop invariants for local stack-allocated buffers. Resolves #716 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent 1e4c7d6 commit 346d59e

File tree

7 files changed

+44
-44
lines changed

7 files changed

+44
-44
lines changed

‎mldsa/src/fips202/fips202x4.h‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ __contract__(
3737
requires(memory_no_alias(in1, inlen))
3838
requires(memory_no_alias(in2, inlen))
3939
requires(memory_no_alias(in3, inlen))
40-
assigns(object_whole(state))
40+
assigns(memory_slice(state, sizeof(mld_shake128x4ctx)))
4141
);
4242

4343
#define mld_shake128x4_squeezeblocks MLD_NAMESPACE(shake128x4_squeezeblocks)
@@ -55,7 +55,7 @@ __contract__(
5555
memory_slice(out1, nblocks * SHAKE128_RATE),
5656
memory_slice(out2, nblocks * SHAKE128_RATE),
5757
memory_slice(out3, nblocks * SHAKE128_RATE),
58-
object_whole(state))
58+
memory_slice(state, sizeof(mld_shake128x4ctx)))
5959
);
6060

6161
#define mld_shake128x4_init MLD_NAMESPACE(shake128x4_init)
@@ -76,7 +76,7 @@ __contract__(
7676
requires(memory_no_alias(in1, inlen))
7777
requires(memory_no_alias(in2, inlen))
7878
requires(memory_no_alias(in3, inlen))
79-
assigns(object_whole(state))
79+
assigns(memory_slice(state, sizeof(mld_shake256x4ctx)))
8080
);
8181

8282
#define mld_shake256x4_squeezeblocks MLD_NAMESPACE(shake256x4_squeezeblocks)
@@ -94,7 +94,7 @@ __contract__(
9494
memory_slice(out1, nblocks * SHAKE256_RATE),
9595
memory_slice(out2, nblocks * SHAKE256_RATE),
9696
memory_slice(out3, nblocks * SHAKE256_RATE),
97-
object_whole(state))
97+
memory_slice(state, sizeof(mld_shake256x4ctx)))
9898
);
9999

100100
#define mld_shake256x4_init MLD_NAMESPACE(shake256x4_init)

‎mldsa/src/packing.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ void mld_pack_pk(uint8_t pk[CRYPTO_PUBLICKEYBYTES],
2727

2828
for (i = 0; i < MLDSA_K; ++i)
2929
__loop__(
30-
assigns(i, object_whole(pk))
30+
assigns(i, memory_slice(pk, CRYPTO_PUBLICKEYBYTES))
3131
invariant(i <= MLDSA_K)
3232
)
3333
{
@@ -186,7 +186,7 @@ static int mld_unpack_hints(
186186
__contract__(
187187
requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES))
188188
requires(memory_no_alias(h, sizeof(mld_polyveck)))
189-
assigns(object_whole(h))
189+
assigns(memory_slice(h, sizeof(mld_polyveck)))
190190
/* All returned coefficients are either 0 or 1 */
191191
ensures(forall(k1, 0, MLDSA_K,
192192
array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))

‎mldsa/src/packing.h‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ __contract__(
2727
requires(memory_no_alias(t1, sizeof(mld_polyveck)))
2828
requires(forall(k0, 0, MLDSA_K,
2929
array_bound(t1->vec[k0].coeffs, 0, MLDSA_N, 0, 1 << 10)))
30-
assigns(object_whole(pk))
30+
assigns(memory_slice(pk, CRYPTO_PUBLICKEYBYTES))
3131
);
3232

3333

@@ -65,7 +65,7 @@ __contract__(
6565
array_abs_bound(s1->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
6666
requires(forall(k2, 0, MLDSA_K,
6767
array_abs_bound(s2->vec[k2].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
68-
assigns(object_whole(sk))
68+
assigns(memory_slice(sk, CRYPTO_SECRETKEYBYTES))
6969
);
7070

7171

@@ -121,8 +121,8 @@ __contract__(
121121
requires(memory_no_alias(pk, CRYPTO_PUBLICKEYBYTES))
122122
requires(memory_no_alias(rho, MLDSA_SEEDBYTES))
123123
requires(memory_no_alias(t1, sizeof(mld_polyveck)))
124-
assigns(object_whole(rho))
125-
assigns(object_whole(t1))
124+
assigns(memory_slice(rho, MLDSA_SEEDBYTES))
125+
assigns(memory_slice(t1, sizeof(mld_polyveck)))
126126
ensures(forall(k0, 0, MLDSA_K,
127127
array_bound(t1->vec[k0].coeffs, 0, MLDSA_N, 0, 1 << 10)))
128128
);
@@ -155,12 +155,12 @@ __contract__(
155155
requires(memory_no_alias(s1, sizeof(mld_polyvecl)))
156156
requires(memory_no_alias(s2, sizeof(mld_polyveck)))
157157
requires(memory_no_alias(sk, CRYPTO_SECRETKEYBYTES))
158-
assigns(object_whole(rho))
159-
assigns(object_whole(tr))
160-
assigns(object_whole(key))
161-
assigns(object_whole(t0))
162-
assigns(object_whole(s1))
163-
assigns(object_whole(s2))
158+
assigns(memory_slice(rho, MLDSA_SEEDBYTES))
159+
assigns(memory_slice(tr, MLDSA_TRBYTES))
160+
assigns(memory_slice(key, MLDSA_SEEDBYTES))
161+
assigns(memory_slice(t0, sizeof(mld_polyveck)))
162+
assigns(memory_slice(s1, sizeof(mld_polyvecl)))
163+
assigns(memory_slice(s2, sizeof(mld_polyveck)))
164164
ensures(forall(k0, 0, MLDSA_K,
165165
array_bound(t0->vec[k0].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)))
166166
ensures(forall(k1, 0, MLDSA_L,
@@ -191,9 +191,9 @@ __contract__(
191191
requires(memory_no_alias(c, MLDSA_CTILDEBYTES))
192192
requires(memory_no_alias(z, sizeof(mld_polyvecl)))
193193
requires(memory_no_alias(h, sizeof(mld_polyveck)))
194-
assigns(object_whole(c))
195-
assigns(object_whole(z))
196-
assigns(object_whole(h))
194+
assigns(memory_slice(c, MLDSA_CTILDEBYTES))
195+
assigns(memory_slice(z, sizeof(mld_polyvecl)))
196+
assigns(memory_slice(h, sizeof(mld_polyveck)))
197197
ensures(forall(k0, 0, MLDSA_L,
198198
array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
199199
ensures(forall(k1, 0, MLDSA_K,

‎mldsa/src/poly.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -291,7 +291,7 @@ __contract__(
291291
requires(memory_no_alias(r, MLDSA_POLYT1_PACKEDBYTES))
292292
requires(memory_no_alias(a, sizeof(mld_poly)))
293293
requires(array_bound(a->coeffs, 0, MLDSA_N, 0, 1 << 10))
294-
assigns(object_whole(r))
294+
assigns(memory_slice(r, MLDSA_POLYT1_PACKEDBYTES))
295295
);
296296

297297
#define mld_polyt1_unpack MLD_NAMESPACE(polyt1_unpack)

‎mldsa/src/poly_kl.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -310,7 +310,7 @@ __contract__(
310310
requires(memory_no_alias(r, MLDSA_POLYZ_PACKEDBYTES))
311311
requires(memory_no_alias(a, sizeof(mld_poly)))
312312
requires(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
313-
assigns(object_whole(r))
313+
assigns(memory_slice(r, MLDSA_POLYZ_PACKEDBYTES))
314314
);
315315

316316

@@ -350,7 +350,7 @@ __contract__(
350350
requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES))
351351
requires(memory_no_alias(a, sizeof(mld_poly)))
352352
requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
353-
assigns(object_whole(r))
353+
assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES))
354354
);
355355

356356
#endif /* !MLD_POLY_KL_H */

‎mldsa/src/polyvec.c‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ __contract__(
4040
requires(memory_no_alias(mat, MLDSA_K * sizeof(mld_polyvecl)))
4141
requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
4242
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
43-
assigns(object_whole(mat))
43+
assigns(memory_slice(mat, sizeof(mld_polyvecl)*MLDSA_K))
4444
ensures(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
4545
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
4646
)
@@ -390,7 +390,7 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
390390

391391
for (i = 0; i < MLDSA_N; i++)
392392
__loop__(
393-
assigns(i, j, object_whole(w))
393+
assigns(i, j, memory_slice(w, sizeof(mld_poly)))
394394
invariant(i <= MLDSA_N)
395395
invariant(array_abs_bound(w->coeffs, 0, i, MLDSA_Q))
396396
)
@@ -686,7 +686,7 @@ unsigned int mld_polyveck_make_hint(mld_polyveck *h, const mld_polyveck *v0,
686686

687687
for (i = 0; i < MLDSA_K; ++i)
688688
__loop__(
689-
assigns(i, s, object_whole(h))
689+
assigns(i, s, memory_slice(h, sizeof(mld_polyveck)))
690690
invariant(i <= MLDSA_K)
691691
invariant(s <= i * MLDSA_N)
692692
invariant(forall(k1, 0, i, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
@@ -733,7 +733,7 @@ void mld_polyveck_pack_w1(uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
733733

734734
for (i = 0; i < MLDSA_K; ++i)
735735
__loop__(
736-
assigns(i, object_whole(r))
736+
assigns(i, memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
737737
invariant(i <= MLDSA_K)
738738
)
739739
{
@@ -749,7 +749,7 @@ void mld_polyveck_pack_eta(uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES],
749749
mld_assert_abs_bound_2d(p->vec, MLDSA_K, MLDSA_N, MLDSA_ETA + 1);
750750
for (i = 0; i < MLDSA_K; ++i)
751751
__loop__(
752-
assigns(i, object_whole(r))
752+
assigns(i, memory_slice(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES))
753753
invariant(i <= MLDSA_K)
754754
)
755755
{
@@ -765,7 +765,7 @@ void mld_polyvecl_pack_eta(uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES],
765765
mld_assert_abs_bound_2d(p->vec, MLDSA_L, MLDSA_N, MLDSA_ETA + 1);
766766
for (i = 0; i < MLDSA_L; ++i)
767767
__loop__(
768-
assigns(i, object_whole(r))
768+
assigns(i, memory_slice(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))
769769
invariant(i <= MLDSA_L)
770770
)
771771
{
@@ -782,7 +782,7 @@ void mld_polyvecl_pack_z(uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES],
782782
MLDSA_GAMMA1 + 1);
783783
for (i = 0; i < MLDSA_L; ++i)
784784
__loop__(
785-
assigns(i, object_whole(r))
785+
assigns(i, memory_slice(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES))
786786
invariant(i <= MLDSA_L)
787787
)
788788
{
@@ -799,7 +799,7 @@ void mld_polyveck_pack_t0(uint8_t r[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES],
799799
(1 << (MLDSA_D - 1)) + 1);
800800
for (i = 0; i < MLDSA_K; ++i)
801801
__loop__(
802-
assigns(i, object_whole(r))
802+
assigns(i, memory_slice(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES))
803803
invariant(i <= MLDSA_K)
804804
)
805805
{

‎mldsa/src/polyvec.h‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ __contract__(
9292
requires(memory_no_alias(v, sizeof(mld_polyvecl)))
9393
requires(forall(k0, 0, MLDSA_L, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < REDUCE32_DOMAIN_MAX)))
9494
requires(forall(k2, 0, MLDSA_L, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
95-
assigns(object_whole(u))
95+
assigns(memory_slice(u, sizeof(mld_polyvecl)))
9696
ensures(forall(k4, 0, MLDSA_L, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == old(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
9797
ensures(forall(k6, 0, MLDSA_L,
9898
array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
@@ -290,7 +290,7 @@ __contract__(
290290
requires(memory_no_alias(v, sizeof(mld_polyveck)))
291291
requires(forall(k0, 0, MLDSA_K, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < REDUCE32_DOMAIN_MAX)))
292292
requires(forall(k2, 0, MLDSA_K, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
293-
assigns(object_whole(u))
293+
assigns(memory_slice(u, sizeof(mld_polyveck)))
294294
ensures(forall(k4, 0, MLDSA_K, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == old(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
295295
ensures(forall(k6, 0, MLDSA_L,
296296
array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
@@ -314,7 +314,7 @@ __contract__(
314314
requires(memory_no_alias(v, sizeof(mld_polyveck)))
315315
requires(forall(k0, 0, MLDSA_K, array_abs_bound(u->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q)))
316316
requires(forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLDSA_Q)))
317-
assigns(object_whole(u))
317+
assigns(memory_slice(u, sizeof(mld_polyveck)))
318318
ensures(forall(k0, 0, MLDSA_K,
319319
array_bound(u->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
320320
);
@@ -507,7 +507,7 @@ __contract__(
507507
requires(memory_no_alias(h, sizeof(mld_polyveck)))
508508
requires(memory_no_alias(v0, sizeof(mld_polyveck)))
509509
requires(memory_no_alias(v1, sizeof(mld_polyveck)))
510-
assigns(object_whole(h))
510+
assigns(memory_slice(h, sizeof(mld_polyveck)))
511511
ensures(return_value <= MLDSA_N * MLDSA_K)
512512
ensures(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
513513
);
@@ -559,7 +559,7 @@ __contract__(
559559
requires(memory_no_alias(w1, sizeof(mld_polyveck)))
560560
requires(forall(k1, 0, MLDSA_K,
561561
array_bound(w1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))))
562-
assigns(object_whole(r))
562+
assigns(memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
563563
);
564564

565565
#define mld_polyveck_pack_eta MLD_NAMESPACE_KL(polyveck_pack_eta)
@@ -581,7 +581,7 @@ __contract__(
581581
requires(memory_no_alias(p, sizeof(mld_polyveck)))
582582
requires(forall(k1, 0, MLDSA_K,
583583
array_abs_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
584-
assigns(object_whole(r))
584+
assigns(memory_slice(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES))
585585
);
586586

587587
#define mld_polyvecl_pack_eta MLD_NAMESPACE_KL(polyvecl_pack_eta)
@@ -603,7 +603,7 @@ __contract__(
603603
requires(memory_no_alias(p, sizeof(mld_polyvecl)))
604604
requires(forall(k1, 0, MLDSA_L,
605605
array_abs_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
606-
assigns(object_whole(r))
606+
assigns(memory_slice(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))
607607
);
608608

609609
#define mld_polyvecl_pack_z MLD_NAMESPACE_KL(polyvecl_pack_z)
@@ -625,7 +625,7 @@ __contract__(
625625
requires(memory_no_alias(p, sizeof(mld_polyvecl)))
626626
requires(forall(k1, 0, MLDSA_L,
627627
array_bound(p->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
628-
assigns(object_whole(r))
628+
assigns(memory_slice(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES))
629629
);
630630

631631
#define mld_polyveck_pack_t0 MLD_NAMESPACE_KL(polyveck_pack_t0)
@@ -647,7 +647,7 @@ __contract__(
647647
requires(memory_no_alias(p, sizeof(mld_polyveck)))
648648
requires(forall(k0, 0, MLDSA_K,
649649
array_bound(p->vec[k0].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)))
650-
assigns(object_whole(r))
650+
assigns(memory_slice(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES))
651651
);
652652

653653
#define mld_polyvecl_unpack_eta MLD_NAMESPACE_KL(polyvecl_unpack_eta)
@@ -667,7 +667,7 @@ void mld_polyvecl_unpack_eta(
667667
__contract__(
668668
requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))
669669
requires(memory_no_alias(p, sizeof(mld_polyvecl)))
670-
assigns(object_whole(p))
670+
assigns(memory_slice(p, sizeof(mld_polyvecl)))
671671
ensures(forall(k1, 0, MLDSA_L,
672672
array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)))
673673
);
@@ -689,7 +689,7 @@ void mld_polyvecl_unpack_z(mld_polyvecl *z,
689689
__contract__(
690690
requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES))
691691
requires(memory_no_alias(z, sizeof(mld_polyvecl)))
692-
assigns(object_whole(z))
692+
assigns(memory_slice(z, sizeof(mld_polyvecl)))
693693
ensures(forall(k1, 0, MLDSA_L,
694694
array_bound(z->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
695695
);
@@ -711,7 +711,7 @@ void mld_polyveck_unpack_eta(
711711
__contract__(
712712
requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES))
713713
requires(memory_no_alias(p, sizeof(mld_polyveck)))
714-
assigns(object_whole(p))
714+
assigns(memory_slice(p, sizeof(mld_polyveck)))
715715
ensures(forall(k1, 0, MLDSA_K,
716716
array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)))
717717
);
@@ -733,7 +733,7 @@ void mld_polyveck_unpack_t0(mld_polyveck *p,
733733
__contract__(
734734
requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES))
735735
requires(memory_no_alias(p, sizeof(mld_polyveck)))
736-
assigns(object_whole(p))
736+
assigns(memory_slice(p, sizeof(mld_polyveck)))
737737
ensures(forall(k1, 0, MLDSA_K,
738738
array_bound(p->vec[k1].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)))
739739
);
@@ -795,7 +795,7 @@ __contract__(
795795
array_bound(mat[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
796796
requires(forall(l1, 0, MLDSA_L,
797797
array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
798-
assigns(object_whole(t))
798+
assigns(memory_slice(t, sizeof(mld_polyveck)))
799799
ensures(forall(k0, 0, MLDSA_K,
800800
array_abs_bound(t->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q)))
801801
);

0 commit comments

Comments
 (0)