check-magic: Remember all explained magic constants

Previously, scripts/check-magic would remember only the last explained
magic constant, preventing, for example, the explanation of multiple
magic constants ahead of a comment block referring to all of them.

Moreover, check-magic would only lazily evaluate a provided explanation
when actually finding a magic value magic the LHS of the proposed
explanation. In particular, a _wrong_ explanation would only be caught
if, in the rest of the file under consideration, some matching magic
constant would be found. This led to an ambiguous and unused explanation
being overlooked in params.h.

This commit makes check-magic more general so that
- it always checks magic value explanations when they are provided,
  regardless of whether they are needed or not; and,
- it remembers all magic values explained so far.

Moreover, the `round` function is instrumented to fail if it is
called on an odd multiple of 1/2 -- in this case, the rounding
is ambiguous (do we want round-half-down or round-half-up?);
this was the source of the mismatch in params.h previously.

We also add support for `intdiv(a,b)` to an integer division which we
want to assert to be without residue. This can be used instead of `//`
to additionally check that the division is indeed integral.

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

Author: hanno-becker

mldsa/src/params.h

@@ -13,7 +13,6 @@
 #define MLDSA_RNDBYTES 32
 #define MLDSA_N 256
 #define MLDSA_Q 8380417
-/* check-magic: 4190209 == round(MLDSA_Q/2) */
 #define MLDSA_Q_HALF ((MLDSA_Q + 1) / 2)
 #define MLDSA_D 13
 

scripts/check-magic

@@ -8,9 +8,10 @@
 #
 
 import re
+import math
 import pathlib
 
-from sympy import simplify, sympify, Function
+from sympy import simplify, sympify, Function, Rational
 
 def get_c_source_files():
     return get_files("mldsa/**/*.c")
@@ -21,6 +22,17 @@ def get_header_files():
 def get_files(pattern):
     return list(map(str, pathlib.Path().glob(pattern)))
 
+# Standard color definitions
+GREEN="\033[32m"
+RED="\033[31m"
+BLUE="\033[94m"
+BOLD="\033[1m"
+NORMAL="\033[0m"
+
+CHECKED = f"{GREEN}✓{NORMAL}"
+FAIL = f"{RED}✗{NORMAL}"
+REMEMBERED = f"{BLUE}⊢{NORMAL}"
+
 def check_magic_numbers():
     mldsa_q = 8380417
     exceptions = [mldsa_q]
@@ -62,9 +74,21 @@ def check_magic_numbers():
             y = int(y)
             m = int(m)
             return signed_mod(pow(x,y,m),m)
+        def safe_round(x):
+            if x - math.floor(x) == Rational(1, 2):
+                raise ValueError(f"Ambiguous rounding: {x} is an odd multiple of 0.5 and it is unclear if round-up or round-down is desired")
+            return round(x)
+        def safe_floordiv(x, y):
+            x = int(x)
+            y = int(y)
+            if x % y != 0:
+                raise ValueError(f"Non-integral division: {x} // {y} has remainder {x % y}")
+            return x // y
         locals_dict = {'signed_mod': signed_mod,
                        'unsigned_mod': unsigned_mod,
-                       'pow': pow_mod }
+                       'pow': pow_mod,
+                       'round': safe_round,
+                       'intdiv': safe_floordiv }
         locals_dict.update(known_magics)
         return sympify(m, locals=locals_dict)
 
@@ -80,6 +104,7 @@ def check_magic_numbers():
         enabled = True
         magic_dict = {'MLDSA_Q': mldsa_q, 'REDUCE32_DOMAIN_MAX': 2143289343}
         magic_expr = None
+        verified_magics = {}
         for i, l in enumerate(content):
             if enabled is True and disable_marker in l:
                 enabled = False
@@ -92,6 +117,12 @@ def check_magic_numbers():
             l, g = get_magic(l)
             if g is not None:
                 magic_val, magic_expr = g
+                magic_val_check = evaluate_magic(magic_expr, magic_dict)
+                if magic_val != magic_val_check:
+                    print(f"{FAIL}:{filename}:{i+1}: Mismatching magic annotation: {magic_val} != {magic_expr} (= {magic_val_check})")
+                    exit(1)
+                print(f"{REMEMBERED}:{filename}:{i+1}: Verified explanation {magic_val} == {magic_expr}")
+                verified_magics[magic_val] = magic_expr
 
             found = next(re.finditer(pattern, l), None)
             if found is None:
@@ -101,16 +132,12 @@ def check_magic_numbers():
             if is_exception(filename, l, magic):
                 continue
 
-            if magic_expr is not None:
-                val = evaluate_magic(magic_expr, magic_dict)
-                if magic_val != val:
-                    raise Exception(f"{filename}:{i}: Mismatching magic annotation: {magic_val} != {val}")
-                if val == magic:
-                    print(f"[OK] {filename}:{i}: Verified magic constant {magic} == {magic_expr}")
-                else:
-                    raise Exception(f"{filename}:{i}: Magic constant mismatch {magic} != {magic_expr}")
-            else:
-                raise Exception(f"{filename}:{i}: No explanation for magic value {magic}")
+            explanation = verified_magics.get(magic, None)
+            if explanation is None:
+                print(f"{FAIL}:{filename}:{i+1}: No explanation for magic value {magic}")
+                exit(1)
+
+            print(f"{CHECKED}:{filename}:{i+1}: {magic} previously explained as {explanation}")
 
             # If this is a #define's clause, remember it
             define = get_define(l)