Add a safety sanity-check.

.github/workflows/safety.yml

@@ -0,0 +1,19 @@
+name: "Safety sanity-check"
+on:
+  pull_request:
+  push:
+
+jobs:
+  tests:
+    name: tests
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v25
+      with:
+        nix_path: nixpkgs=channel:nixos-unstable
+    - uses: DeterminateSystems/magic-nix-cache-action@v3
+    - run: nix-shell --run 'echo Installed dependencies.'
+    - run: nix-shell --run 'make run-interpreter'

Makefile

@@ -39,6 +39,10 @@ check-ct: $(IMPLEMENTATION)/ml_dsa.jazz
 check-sct: $(IMPLEMENTATION)/ml_dsa.jazz
 	$(JASMINCT) --speculative $^
 
+.PHONY: run-interpreter
+run-interpreter: $(IMPLEMENTATION)/test/execute.jazz $(IMPLEMENTATION)/ml_dsa.jazz
+	$(JASMINC) $^ | grep 'true'
+
 # --------------------------------------------------------------------
 bench.o: $(OUTPUT_FILE_NAME).s bench/bench.c bench/notrandombytes.c $(IMPLEMENTATION)/api.h
 	$(CC) -Wall -Werror \

ref/ml_dsa_65/test/execute.jazz

@@ -0,0 +1,20 @@
+/* The correctness of the transformations applied by Jasmin when compiling code
+ * relies on the input code not having undefined behaviour. Running our implementation
+ * through the interpreter is a sanity-check: If we run the interpreter without
+ * crashing the program, at least for the inputs we've given it in "runner.jazz",
+ * the program is correct.
+ *
+ * Ideally, we'd want to run the implementation through a safety-checker, but this
+ * checker is outdated and takes an inordinate amount of time to run (on the order
+ * of several days).
+*/
+
+require "runner.jazz"
+
+exec test_consistency (
+  0x1000:1952,
+  0x2000:4032,
+  0x3000:3309,
+  0x4000:64, // Message size
+  0x5000:64 // Total randomness
+)

ref/ml_dsa_65/test/runner.jazz

@@ -0,0 +1,58 @@
+require "../ml_dsa.jazz"
+
+inline fn setup_memory() -> reg u64, reg u64, reg u64, reg u64, reg u64, reg u64
+{
+    reg u64 verification_key signing_key signature message message_size randomness;
+
+    inline int i;
+
+    verification_key = 0x1000;
+    signing_key = 0x2000;
+
+    signature = 0x3000;
+
+    message = 0x4000;
+    message_size = 64;
+
+    randomness = 0x5000;
+
+    for i = 0 to 8 {
+        [randomness + 8 * i] = i;
+        [message + 8 * i] = i;
+    }
+
+    return verification_key, signing_key, signature, message, message_size, randomness;
+}
+
+fn test_consistency() -> reg bool {
+    reg u64 verification_key signing_key signature message message_size randomness;
+    verification_key, signing_key, signature, message, message_size, randomness = setup_memory();
+
+    reg u64 verify_result i;
+
+    stack u8[32] keygen_randomness signing_randomness;
+
+    i = 0;
+    while (i < 32) {
+        keygen_randomness[i] = (u8)[randomness + i];
+        signing_randomness[i] = (u8)[randomness + i + 32];
+
+        i += 1;
+    }
+
+    #[inline]
+    ml_dsa_65_keygen(verification_key, signing_key, keygen_randomness);
+    #[inline]
+    ml_dsa_65_sign(signature, signing_key, message, message_size, signing_randomness);
+    #[inline]
+    verify_result = ml_dsa_65_verify(verification_key, message, message_size, signature);
+
+    reg bool result;
+    if (verify_result == 0) {
+        result = true;
+    } else {
+        result = false;
+    }
+
+    return result;
+}