From 20dbffb4ef4fd6f916080c0881d40cd3d523029c Mon Sep 17 00:00:00 2001
From: Hanno Becker <beckphan@amazon.co.uk>
Date: Thu, 31 Oct 2024 05:50:03 +0000
Subject: [PATCH] Add debug assertion for checking scalar bounds

We already have `mlkem_debug_check_bounds()` to check
bounds on all elements of an array.

In preparation for use in `fqmul()`, this commit adds
generic `mlkem_debug_assert()` and `ASSERT()` to checking
assertions, and a wrapper assertion `SCALAR_BOUND` to assert
absolute bounds on scalars.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
---
 mlkem/debug/debug.c | 10 ++++++++++
 mlkem/debug/debug.h | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+)

diff --git a/mlkem/debug/debug.c b/mlkem/debug/debug.c
index 94a5dbe7e..acb83f124 100644
--- a/mlkem/debug/debug.c
+++ b/mlkem/debug/debug.c
@@ -5,6 +5,16 @@
 
 static char debug_buf[256];
 
+void mlkem_debug_assert(const char *file, int line,
+                        const char *description, const int val) {
+  if (val == 0)
+  {
+    snprintf(debug_buf, sizeof(debug_buf),
+             "Assertion failed: %s (value %d)", description, val);
+    mlkem_debug_print_error(file, line, debug_buf);
+    exit(1);
+  }
+}
 void mlkem_debug_check_bounds(const char *file, int line,
                               const char *description, const int16_t *ptr,
                               unsigned len, int lower_bound_exclusive,
diff --git a/mlkem/debug/debug.h b/mlkem/debug/debug.h
index bcbc70ee8..958e09402 100644
--- a/mlkem/debug/debug.h
+++ b/mlkem/debug/debug.h
@@ -7,6 +7,22 @@
 #include <stdio.h>
 #include <stdlib.h>
 
+/*************************************************
+ * Name:        mlkem_debug_assert
+ *
+ * Description: Check debug assertion
+ *
+ *              Prints an error message to stderr and calls
+ *              exit(1) if not.
+ *
+ * Arguments:   - file: filename
+ *              - line: line number
+ *              - description: Textual description of assertion
+ *              - val: Value asserted to be non-zero
+ **************************************************/
+void mlkem_debug_assert(const char *file, int line,
+                        const char *description, const int val);
+
 /*************************************************
  * Name:        mlkem_debug_check_bounds
  *
@@ -32,6 +48,25 @@ void mlkem_debug_check_bounds(const char *file, int line,
 /* Print error message to stderr alongside file and line information */
 void mlkem_debug_print_error(const char *file, int line, const char *msg);
 
+/* Check assertion, calling exit() upon failure
+ *
+ * val: Value that's asserted to be non-zero
+ * msg: Message to print on failure
+ *
+ * Currently called CASSERT to avoid clash with CBMC assert.
+ */
+#define CASSERT(val, msg)                                                 \
+  do {                                                                    \
+      mlkem_debug_assert(__FILE__, __LINE__, (msg), (val));               \
+  } while (0)
+
+/* Check absolute bounds of scalar
+ * val: Scalar to be checked
+ * abs_bound: Exclusive upper bound on absolute value to check
+ * msg: Message to print on failure */
+#define SCALAR_BOUND(val, abs_bound, msg)                       \
+  CASSERT((val) > -(abs_bound) && (val) < (abs_bound), msg)
+
 /* Check that all coefficients in array of int16_t's are non-negative
  * and below an exclusive upper bound.
  *
@@ -127,6 +162,12 @@ void mlkem_debug_print_error(const char *file, int line, const char *msg);
 
 #else /* MLKEM_DEBUG */
 
+#define CASSERT(...) \
+  do {             \
+  } while (0)
+#define SCALAR_BOUND(...) \
+  do {             \
+  } while (0)
 #define BOUND(...) \
   do {             \
   } while (0)