Remove output bound for poly_mulcache_compute

The higher level functions do not require a output bound for
poly_mulcache_compute.
However, all our backend (C/AVX2/Arm64) produce outputs in (-q,q) and hence
the lower level functions did have according assertions or post-conditions.

The HOL-Light proof for the AArch64 implementation of poly_mulcache_compute,
however, does not prove a output bound for it.
We are considering adding a post-condition, but that is some work:
#1032

For the meantime, this commit removes the post-condition from the lower level
functions such that it is consistent with the HOL-Light proof.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
the contracts of the lower level functions

Author: mkannwischer

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -93,7 +93,6 @@ __contract__(
   requires(zetas == mlk_aarch64_zetas_mulcache_native)
   requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
   assigns(object_whole(cache))
-  ensures(array_abs_bound(cache, 0, MLKEM_N / 2, MLKEM_Q))
 );
 
 #define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -93,7 +93,6 @@ __contract__(
   requires(zetas == mlk_aarch64_zetas_mulcache_native)
   requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
   assigns(object_whole(cache))
-  ensures(array_abs_bound(cache, 0, MLKEM_N / 2, MLKEM_Q))
 );
 
 #define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)

mlkem/native/aarch64/src/arith_native_aarch64.h

@@ -93,7 +93,6 @@ __contract__(
   requires(zetas == mlk_aarch64_zetas_mulcache_native)
   requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
   assigns(object_whole(cache))
-  ensures(array_abs_bound(cache, 0, MLKEM_N / 2, MLKEM_Q))
 );
 
 #define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)

mlkem/native/api.h

@@ -209,7 +209,6 @@ __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))
-  ensures(array_abs_bound(cache, 0, MLKEM_N / 2, MLKEM_Q))
 );
 #endif /* MLK_USE_NATIVE_POLY_MULCACHE_COMPUTE */
 

mlkem/poly.c

@@ -283,12 +283,6 @@ MLK_INTERNAL_API
 void mlk_poly_mulcache_compute(mlk_poly_mulcache *x, const mlk_poly *a)
 {
   mlk_poly_mulcache_compute_native(x->coeffs, a->coeffs);
-  /*
-   * This bound is true for the AArch64 and AVX2 implementations,
-   * but not needed in the higher level bounds reasoning.
-   * It is thus omitted from the spec but checked here nonetheless.
-   */
-  mlk_assert_abs_bound(x, MLKEM_N / 2, MLKEM_Q);
 }
 #endif /* MLK_USE_NATIVE_POLY_MULCACHE_COMPUTE */