CBMC: Remove uses of object_whole and same_object

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -94,7 +94,7 @@ __contract__(
   requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
   requires(zetas == mlk_aarch64_zetas_mulcache_native)
   requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
-  assigns(object_whole(cache))
+  assigns(memory_slice(cache, sizeof(int16_t) * (MLKEM_N / 2)))
   ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
 );
 
@@ -106,7 +106,7 @@ __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
   requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, MLKEM_POLYBYTES))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -93,7 +93,7 @@ __contract__(
   requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
   requires(zetas == mlk_aarch64_zetas_mulcache_native)
   requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
-  assigns(object_whole(cache))
+  assigns(memory_slice(cache, sizeof(int16_t) * (MLKEM_N / 2)))
   ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
 );
 
@@ -105,7 +105,7 @@ __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
   requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, MLKEM_POLYBYTES))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \

mlkem/src/cbmc.h

@@ -50,7 +50,6 @@
  */
 #define object_whole(...) __CPROVER_object_whole(__VA_ARGS__)
 #define memory_slice(...) __CPROVER_object_upto(__VA_ARGS__)
-#define same_object(...) __CPROVER_same_object(__VA_ARGS__)
 
 /*
  * Pointer-related predicates

mlkem/src/compress.c

@@ -457,7 +457,7 @@ __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(mlk_poly)))
   requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, MLKEM_POLYBYTES))
 )
 {
   unsigned i;

mlkem/src/compress.h

@@ -598,7 +598,7 @@ __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(mlk_poly)))
   requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, MLKEM_POLYBYTES))
 );
 
 
@@ -654,7 +654,7 @@ void mlk_poly_frommsg(mlk_poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES])
 __contract__(
   requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES))
   requires(memory_no_alias(r, sizeof(mlk_poly)))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, sizeof(mlk_poly)))
   ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
 );
 
@@ -683,7 +683,7 @@ __contract__(
   requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES))
   requires(memory_no_alias(r, sizeof(mlk_poly)))
   requires(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
-  assigns(object_whole(msg))
+  assigns(memory_slice(msg, MLKEM_INDCPA_MSGBYTES))
 );
 
 #endif /* !MLK_COMPRESS_H */

mlkem/src/fips202/fips202x4.h

@@ -30,7 +30,7 @@ __contract__(
   requires(memory_no_alias(in1, inlen))
   requires(memory_no_alias(in2, inlen))
   requires(memory_no_alias(in3, inlen))
-  assigns(object_whole(state))
+  assigns(memory_slice(state, sizeof(mlk_shake128x4ctx)))
 );
 
 #define mlk_shake128x4_squeezeblocks MLK_NAMESPACE(shake128x4_squeezeblocks)
@@ -48,7 +48,7 @@ __contract__(
     memory_slice(out1, nblocks * SHAKE128_RATE),
     memory_slice(out2, nblocks * SHAKE128_RATE),
     memory_slice(out3, nblocks * SHAKE128_RATE),
-    object_whole(state))
+    memory_slice(state, sizeof(mlk_shake128x4ctx)))
 );
 
 #define mlk_shake128x4_init MLK_NAMESPACE(shake128x4_init)

mlkem/src/indcpa.c

@@ -222,14 +222,14 @@ __contract__(
   requires(memory_no_alias(a, sizeof(mlk_polymat)))
   requires(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
     array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
-  assigns(object_whole(a))
+  assigns(memory_slice(a, sizeof(mlk_polymat)))
   ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
     array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
 {
   unsigned i;
   for (i = 0; i < MLKEM_K; i++)
   __loop__(
-     assigns(i, object_whole(a))
+     assigns(i, memory_slice(a, sizeof(mlk_polymat)))
      invariant(i <= MLKEM_K)
      invariant(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
        array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
@@ -354,12 +354,12 @@ __contract__(
   requires(forall(k0, 0, MLKEM_K,
     forall(k1, 0, MLKEM_K,
       array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))))
-  assigns(object_whole(out)))
+  assigns(memory_slice(out, sizeof(mlk_polyvec))))
 {
   unsigned i;
   for (i = 0; i < MLKEM_K; i++)
   __loop__(
-    assigns(i, object_whole(out))
+    assigns(i, memory_slice(out, sizeof(mlk_polyvec)))
     invariant(i <= MLKEM_K))
   {
     mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc);

mlkem/src/indcpa.h

@@ -45,7 +45,7 @@ __contract__(
   requires(memory_no_alias(a, sizeof(mlk_polymat)))
   requires(memory_no_alias(seed, MLKEM_SYMBYTES))
   requires(transposed == 0 || transposed == 1)
-  assigns(object_whole(a))
+  assigns(memory_slice(a, sizeof(mlk_polymat)))
   ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
   array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
 );
@@ -75,8 +75,8 @@ __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES))
   requires(memory_no_alias(coins, MLKEM_SYMBYTES))
-  assigns(object_whole(pk))
-  assigns(object_whole(sk))
+  assigns(memory_slice(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
+  assigns(memory_slice(sk, MLKEM_INDCPA_SECRETKEYBYTES))
 );
 
 #define mlk_indcpa_enc MLK_NAMESPACE_K(indcpa_enc)
@@ -109,7 +109,7 @@ __contract__(
   requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES))
   requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
   requires(memory_no_alias(coins, MLKEM_SYMBYTES))
-  assigns(object_whole(c))
+  assigns(memory_slice(c, MLKEM_INDCPA_BYTES))
 );
 
 #define mlk_indcpa_dec MLK_NAMESPACE_K(indcpa_dec)
@@ -137,7 +137,7 @@ __contract__(
   requires(memory_no_alias(c, MLKEM_INDCPA_BYTES))
   requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES))
-  assigns(object_whole(m))
+  assigns(memory_slice(m, MLKEM_INDCPA_MSGBYTES))
 );
 
 #endif /* !MLK_INDCPA_H */

mlkem/src/kem.h

@@ -143,8 +143,8 @@ __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
   requires(memory_no_alias(coins, 2 * MLKEM_SYMBYTES))
-  assigns(object_whole(pk))
-  assigns(object_whole(sk))
+  assigns(memory_slice(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
+  assigns(memory_slice(sk, MLKEM_INDCCA_SECRETKEYBYTES))
 );
 
 /*************************************************
@@ -173,8 +173,8 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
 __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
-  assigns(object_whole(pk))
-  assigns(object_whole(sk))
+  assigns(memory_slice(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
+  assigns(memory_slice(sk, MLKEM_INDCCA_SECRETKEYBYTES))
 );
 
 /*************************************************
@@ -213,8 +213,8 @@ __contract__(
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   requires(memory_no_alias(coins, MLKEM_SYMBYTES))
-  assigns(object_whole(ct))
-  assigns(object_whole(ss))
+  assigns(memory_slice(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
+  assigns(memory_slice(ss, MLKEM_SSBYTES))
 );
 
 /*************************************************
@@ -248,8 +248,8 @@ __contract__(
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
-  assigns(object_whole(ct))
-  assigns(object_whole(ss))
+  assigns(memory_slice(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
+  assigns(memory_slice(ss, MLKEM_SSBYTES))
 );
 
 /*************************************************
@@ -283,7 +283,7 @@ __contract__(
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
-  assigns(object_whole(ss))
+  assigns(memory_slice(ss, MLKEM_SSBYTES))
 );
 
 #endif /* !MLK_KEM_H */

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

@@ -93,7 +93,7 @@ __contract__(
   requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
   requires(zetas == mlk_aarch64_zetas_mulcache_native)
   requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
-  assigns(object_whole(cache))
+  assigns(memory_slice(cache, sizeof(int16_t) * (MLKEM_N / 2)))
   ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
 );
 
@@ -105,7 +105,7 @@ __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
   requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, MLKEM_POLYBYTES))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \

mlkem/src/native/api.h

@@ -226,7 +226,7 @@ static MLK_INLINE int mlk_poly_mulcache_compute_native(
 __contract__(
   requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
   requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
-  assigns(object_whole(cache))
+  assigns(memory_slice(cache, sizeof(int16_t) * (MLKEM_N / 2)))
   ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
   ensures((return_value == MLK_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
 );
@@ -357,7 +357,7 @@ __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
   requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, MLKEM_POLYBYTES))
   ensures(return_value == MLK_NATIVE_FUNC_SUCCESS || return_value == MLK_NATIVE_FUNC_FALLBACK)
 );
 #endif /* MLK_USE_NATIVE_POLY_TOBYTES */

mlkem/src/poly.c

@@ -276,7 +276,7 @@ MLK_STATIC_TESTABLE void mlk_poly_mulcache_compute_c(mlk_poly_mulcache *x,
 __contract__(
   requires(memory_no_alias(x, sizeof(mlk_poly_mulcache)))
   requires(memory_no_alias(a, sizeof(mlk_poly)))
-  assigns(object_whole(x))
+  assigns(memory_slice(x, sizeof(mlk_poly_mulcache)))
 )
 {
   unsigned i;

mlkem/src/poly.h

@@ -159,7 +159,7 @@ void mlk_poly_mulcache_compute(mlk_poly_mulcache *x, const mlk_poly *a)
 __contract__(
   requires(memory_no_alias(x, sizeof(mlk_poly_mulcache)))
   requires(memory_no_alias(a, sizeof(mlk_poly)))
-  assigns(object_whole(x))
+  assigns(memory_slice(x, sizeof(mlk_poly_mulcache)))
 );
 
 #define mlk_poly_reduce MLK_NAMESPACE(poly_reduce)
@@ -252,7 +252,7 @@ __contract__(
   requires(forall(k0, 0, MLKEM_N, (int32_t) r->coeffs[k0] - b->coeffs[k0] <= INT16_MAX))
   requires(forall(k1, 0, MLKEM_N, (int32_t) r->coeffs[k1] - b->coeffs[k1] >= INT16_MIN))
   ensures(forall(k, 0, MLKEM_N, r->coeffs[k] == old(*r).coeffs[k] - b->coeffs[k]))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, sizeof(mlk_poly)))
 );
 
 #define mlk_poly_ntt MLK_NAMESPACE(poly_ntt)

mlkem/src/poly_k.c

@@ -85,7 +85,7 @@ void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a)
 
   for (i = 0; i < MLKEM_K; i++)
   __loop__(
-    assigns(i, object_whole(r))
+    assigns(i, memory_slice(r, MLKEM_POLYVECBYTES))
     invariant(i <= MLKEM_K)
   )
   {
@@ -157,7 +157,7 @@ __contract__(
   requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
   requires(forall(k1, 0, MLKEM_K,
      array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
-  assigns(object_whole(r))
+  assigns(memory_slice(r, sizeof(mlk_poly)))
 )
 {
   unsigned i;