CBMC: Remove convoluted implementation of 2D bounds check

A previous issue in CBMC

diffblue/cbmc#8570

had forced to break bounds assertions over a 2D array into
nested bounds assertions.

This issue has since been fixed, allowing for the simplification
of the respective assertions, which is what this commit does.

Signed-off-by: Hanno Becker <[email protected]>

Author: hanno-becker

mlkem/debug.h

@@ -87,17 +87,11 @@ void mlk_debug_check_bounds(const char *file, int line, const int16_t *ptr,
 #define mlk_assert_abs_bound(ptr, len, value_abs_bd) \
   cassert(array_abs_bound(((int16_t *)(ptr)), 0, (len), (value_abs_bd)))
 
-/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
- * just use a single flattened array_bound(...) here. */
-#define mlk_assert_bound_2d(ptr, M, N, value_lb, value_ub)             \
-  cassert(forall(kN, 0, (M),                                           \
-                 array_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
-                             (value_lb), (value_ub))))
-
-#define mlk_assert_abs_bound_2d(ptr, M, N, value_abs_bd)                   \
-  cassert(forall(kN, 0, (M),                                               \
-                 array_abs_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
-                                 (value_abs_bd))))
+#define mlk_assert_bound_2d(ptr, M, N, value_lb, value_ub) \
+  mlk_assert_bound((ptr), (N) * (M), (value_lb), (value_ub))
+
+#define mlk_assert_abs_bound_2d(ptr, M, N, value_abs_bd) \
+  mlk_assert_abs_bound((ptr), (N) * (M), (value_abs_bd))
 
 #else /* MLKEM_DEBUG */
 

mlkem/native/api.h

@@ -238,17 +238,7 @@ __contract__(
   requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
   requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
   requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
-  /* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
-   * just use a single flattened array_bound(...) here.
-   *
-   * Once fixed, change to:
-   * ```
-   * requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
-   * ```
-   */
-  requires(forall(kN, 0, 2,					  \
-              array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
-			  0, MLKEM_UINT12_LIMIT)))
+  requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
 );
 #endif /* MLK_MULTILEVEL_BUILD_WITH_SHARED || MLKEM_K == 2 */
@@ -281,17 +271,7 @@ __contract__(
   requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
   requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
   requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
-  /* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
-   * just use a single flattened array_bound(...) here.
-   *
-   * Once fixed, change to:
-   * ```
-   * requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
-   * ```
-   */
-  requires(forall(kN, 0, 3,					  \
-              array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
-			  0, MLKEM_UINT12_LIMIT)))
+  requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
 );
 #endif /* MLK_MULTILEVEL_BUILD_WITH_SHARED || MLKEM_K == 3 */
@@ -324,17 +304,7 @@ __contract__(
   requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
   requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
   requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
-  /* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
-   * just use a single flattened array_bound(...) here.
-   *
-   * Once fixed, change to:
-   * ```
-   * requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
-   * ```
-   */
-  requires(forall(kN, 0, 4,					  \
-              array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
-			  0, MLKEM_UINT12_LIMIT)))
+  requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
 );
 #endif /* MLK_MULTILEVEL_BUILD_WITH_SHARED || MLKEM_K == 4 */