CONTRACTS: is_fresh now tracks separation at the byte level instead of whole objects

[remi-delmas-3000]

When assumed, is_fresh still builds distinct objects. When asserted, it allows for either distinct objects or distinct byte intervals within the same object.

A function

foo(int *a, int *b)
requires(__is_fresh(a, N) && is_fresh(b, M))
{ ... }

is checked under the assumption that a and b are completely distinct objects but can still be used in contexts where a and b are disjoint slices of the same base object.

The same modification is applied to ensures clauses in contract checking mode.

Soundness argument :

The weakening of is_fresh semantics in contract replacement mode is sound because in contract checking mode we still use the stronger semantics of is_fresh, and hence we prove that the function does not perform any operation that would requires pointers to be in the same object to be legal (such as pointer differences or comparisons).

Using the weaker semantics of is_fresh in ensures clauses in contract checking mode is also sound, because the stronger semantics is still used for ensures clauses when replacing call with contracts, so that statements downstream of the contract site cannot perform any operations that would require pointers to be into the same object (even if the function may return such pointers in reality).

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 79.57%. Comparing base (159af34) to head (d4a1c6d).
Report is 6 commits behind head on develop.

Additional details and impacted files

@@            Coverage Diff            @@
##           develop    #8603    +/-   ##
=========================================
  Coverage    79.57%   79.57%            
=========================================
  Files         1733     1733            
  Lines       197826   197826            
  Branches     18197    17996   -201     
=========================================
  Hits        157421   157421            
  Misses       40405    40405            

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[hanno-becker]

Somewhat related: In the context of __CPROVER_requires(__CPROVER_is_fresh(x, N)), the meaning of __CPROVER_assigns(__CPROVER_object_whole(x)) should IMO be restricted to the length-N slice at x. This can be forced by using __CPROVER_object_upto(x, N) (which is what we use exclusively in mlkem-native), but I don't think __CPROVER_assigns(__CPROVER_object_whole(x)) affecting the whole object at the call-site, even though the contract only assumes a length-N slice, is ever what you want? In particular, in a contract

__CPROVER_requires(__CPROVER_is_fresh(x, N))
__CPROVER_requires(__CPROVER_is_fresh(y, M))
__CPROVER_assigns(__CPROVER_object_whole(x))
__CPROVER_assigns(__CPROVER_object_whole(y))

the assigns-clauses clash if x,y point to the same object, which they are now allowed to with this PR.

[hanno-becker]

I tested this PR on mlkem-native pq-code-package/mlkem-native#834 and confirm that it works as intended for our use cases.

[remi-delmas-3000]

__CPROVER_assigns(__CPROVER_object_whole(x)) affecting the whole object at the call-site, even though the contract only assumes a length-N slice, is ever what you want? In particular, in a contract

@hanno-becker We use __CPROVER_object_whole(ptr) internally when inferring side effects of loops and need to widen the loop footprint to a sound superset. For instance when a loop touches both i and arr[i], and arr is itself embedded in some aggregate, and we don't know anything about 'i', we just widen the footprint of the loop to __CPROVER_object_whole(arr) to havoc the whole underlying object.

[hanno-becker]

Just to give a flavor how useful this is, a real-world example from mlkem-native:

Before:

void mlk_poly_getnoise_eta1_4x(mlk_poly *r0, mlk_poly *r1, mlk_poly *r2,
                               mlk_poly *r3, const uint8_t seed[MLKEM_SYMBYTES],
                               uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
                               uint8_t nonce3)
/* Depending on MLKEM_K, the pointers passed to this function belong
   to the same objects, so we cannot use memory_no_alias for r0-r3.

   NOTE: Somehow it is important to use memory_no_alias() first in the
         conjunctions defining each case.
*/
#if MLKEM_K == 2
__contract__(
  requires(memory_no_alias(seed, MLKEM_SYMBYTES))
  requires( /* Case A: r0, r1 consecutive, r2, r3 consecutive */
    (memory_no_alias(r0, 2 * sizeof(mlk_poly)) && memory_no_alias(r2, 2 * sizeof(mlk_poly)) &&
     r1 == r0 + 1 && r3 == r2 + 1 && !same_object(r0, r2)))
  assigns(memory_slice(r0, sizeof(mlk_poly)))
  assigns(memory_slice(r1, sizeof(mlk_poly)))
  assigns(memory_slice(r2, sizeof(mlk_poly)))
  assigns(memory_slice(r3, sizeof(mlk_poly)))
  ensures(
    array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1));
);
#elif MLKEM_K == 4
__contract__(
  requires(memory_no_alias(seed, MLKEM_SYMBYTES))
  requires( /* Case B: r0, r1, r2, r3 consecutive */
    (memory_no_alias(r0, 4 * sizeof(mlk_poly)) && r1 == r0 + 1 && r2 == r0 + 2 && r3 == r0 + 3))
  assigns(memory_slice(r0, sizeof(mlk_poly)))
  assigns(memory_slice(r1, sizeof(mlk_poly)))
  assigns(memory_slice(r2, sizeof(mlk_poly)))
  assigns(memory_slice(r3, sizeof(mlk_poly)))
  ensures(
    array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1));
);
#elif MLKEM_K == 3
__contract__(
  requires(memory_no_alias(seed, MLKEM_SYMBYTES))
  requires( /* Case C: r0, r1, r2 consecutive */
 (memory_no_alias(r0, 3 * sizeof(mlk_poly)) && memory_no_alias(r3, 1 * sizeof(mlk_poly)) &&
  r1 == r0 + 1 && r2 == r0 + 2 && !same_object(r3, r0)))
  assigns(memory_slice(r0, sizeof(mlk_poly)))
  assigns(memory_slice(r1, sizeof(mlk_poly)))
  assigns(memory_slice(r2, sizeof(mlk_poly)))
  assigns(memory_slice(r3, sizeof(mlk_poly)))
  ensures(
    array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1));
);
#endif /* MLKEM_K */

After:

void mlk_poly_getnoise_eta1_4x(mlk_poly *r0, mlk_poly *r1, mlk_poly *r2,
                               mlk_poly *r3, const uint8_t seed[MLKEM_SYMBYTES],
                               uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
                               uint8_t nonce3)
__contract__(
  requires(memory_no_alias(seed, MLKEM_SYMBYTES))
  requires(memory_no_alias(r0, sizeof(mlk_poly)))
  requires(memory_no_alias(r1, sizeof(mlk_poly)))
  requires(memory_no_alias(r2, sizeof(mlk_poly)))
  requires(memory_no_alias(r3, sizeof(mlk_poly)))
  assigns(memory_slice(r0, sizeof(mlk_poly)))
  assigns(memory_slice(r1, sizeof(mlk_poly)))
  assigns(memory_slice(r2, sizeof(mlk_poly)))
  assigns(memory_slice(r3, sizeof(mlk_poly)))
  ensures(
    array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)
    && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1));
);

Thanks @remi-delmas-3000 !

[kroening]

@hanno-becker The new contract really does look pretty!