testing: mlkem_ref pass

.github/workflows/ct.yml

@@ -18,4 +18,4 @@ jobs:
         nix_path: nixpkgs=channel:nixos-unstable
     - uses: DeterminateSystems/magic-nix-cache-action@v3
     - run: nix-shell --arg full false --run "echo Dependencies OK…"
-    - run: nix-shell --arg full false --run "make -C code/jasmin/mlkem_${{matrix.dir}}/ ct"
+    - run: nix-shell --arg full false --run "make -C code/jasmin/mlkem_${{matrix.dir}}/ check-constant-time"

.github/workflows/test.yml

@@ -0,0 +1,21 @@
+name: "Tests"
+on:
+  pull_request:
+  push:
+
+jobs:
+  tests:
+    name: tests
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        dir: [ 'ref']
+    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 --arg full false --run "echo Dependencies OK…"
+    - run: nix-shell --arg full false --run "make -C code/jasmin/mlkem_${{matrix.dir}}/ run-tests"

code/Makefile.conf

@@ -1,8 +1,9 @@
 # -*- Makefile -*-
 
 # --------------------------------------------------------------------
-current_dir := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
+CURRENT_DIR := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
+PROJECT_DIR := $(abspath $(CURRENT_DIR)/../)
 
 # --------------------------------------------------------------------
-JASMINC ?=  $(current_dir)/../jasmin/compiler/jasminc
-JAZZCT ?=  $(current_dir)/../jasmin/compiler/jazzct
+JASMINC   ?= $(abspath $(PROJECT_DIR)/jasmin/compiler/jasminc)
+JASMIN_CT ?= $(abspath $(PROJECT_DIR)/jasmin/compiler/jasmin-ct)

code/jasmin/mlkem_ref/Makefile

@@ -7,118 +7,173 @@ CFLAGS := -Wall -Wextra -g -O3 -fomit-frame-pointer
 JFLAGS := ${JADDFLAGS}
 OS     := $(shell uname -s)
 
-.SECONDARY: jpoly.s jpolyvec.s jfips203.s jindcpa.s jkem.s
-
-default: test speed
-
-test: test/test_poly_compress \
-		  test/test_poly_decompress \
-			test/test_poly_tobytes \
-			test/test_poly_frombytes \
-			test/test_poly_tomsg \
-			test/test_poly_frommsg \
-			test/test_poly_add2 \
-			test/test_poly_sub \
-			test/test_poly_ntt \
-			test/test_poly_invntt \
-			test/test_poly_basemul \
-			test/test_poly_frommont \
-			test/test_poly_reduce \
-			test/test_poly_csubq \
-			test/test_poly_getnoise \
-			test/test_polyvec_compress\
-			test/test_polyvec_decompress\
-			test/test_polyvec_tobytes \
-			test/test_polyvec_frombytes \
-			test/test_polyvec_add2 \
-			test/test_polyvec_ntt \
-			test/test_polyvec_invntt \
-			test/test_polyvec_pointwise_acc \
-			test/test_polyvec_reduce\
-			test/test_polyvec_csubq \
-			test/test_fips202 \
-			test/test_indcpa \
-			test/test_kem
+default: run-tests run-speed
+
+# --
+TESTS_POLY := \
+  test/test_poly_compress \
+  test/test_poly_decompress \
+  test/test_poly_tobytes \
+  test/test_poly_frombytes \
+  test/test_poly_tomsg \
+  test/test_poly_frommsg \
+  test/test_poly_add2 \
+  test/test_poly_sub \
+  test/test_poly_ntt \
+  test/test_poly_invntt \
+  test/test_poly_basemul \
+  test/test_poly_frommont \
+  test/test_poly_reduce \
+  test/test_poly_csubq \
+  test/test_poly_getnoise
+
+TESTS_POLYVEC := \
+  test/test_polyvec_compress \
+  test/test_polyvec_decompress\
+  test/test_polyvec_tobytes \
+  test/test_polyvec_frombytes \
+  test/test_polyvec_add2 \
+  test/test_polyvec_ntt \
+  test/test_polyvec_invntt \
+  test/test_polyvec_pointwise_acc \
+  test/test_polyvec_reduce\
+  test/test_polyvec_csubq
+
+TESTS := \
+  $(TESTS_POLY) \
+  $(TESTS_POLYVEC) \
+  test/test_fips202 \
+  test/test_indcpa \
+  test/test_kem
+
+test: $(TESTS)
 
 speed: test/speed_indcpa
 
-HEADERS = params.h poly.h fips202.h kem.h
+#-- 
 
+HEADERS := \
+  params.h \
+  poly.h \
+  fips202.h \
+  kem.h
 
-JHEADERS = params.jinc \
-				   reduce.jinc \
-           			fips202.jinc \
-					 kem.jinc \
-					 verify.jinc
+C_SOURCES := \
+  poly.c \
+  polyvec.c \
+  cbd.c \
+  fips202.c \
+  ntt.c \
+  reduce.c \
+  symmetric-fips202.c \
+  indcpa.c \
+  kem.c
 
-POLYHEADERS = poly.jinc \
-				zetas.jinc \
+JHEADERS := \
+  params.jinc \
+  reduce.jinc \
+  fips202.jinc \
+  kem.jinc \
+  verify.jinc
 
-POLYVECHEADERS = polyvec.jinc \
-                 gen_matrix.jinc \
+POLYHEADERS := \
+  poly.jinc \
+	zetas.jinc
 
-SOURCES = poly.c polyvec.c cbd.c fips202.c ntt.c reduce.c symmetric-fips202.c indcpa.c kem.c \
+POLYVECHEADERS := \
+  polyvec.jinc \
+  gen_matrix.jinc
 
-test/test_indcpa: test/test_indcpa.c $(HEADERS) $(SOURCES) jindcpa.o
-	$(CC) $(CFLAGS) -o $@ $(SOURCES) jindcpa.o $<
+# --
 
-test/test_kem: test/test_kem.c $(HEADERS) $(SOURCES) $(INCS) jkem.o
-	$(CC) $(CFLAGS) -o $@ $(SOURCES) ~/Desktop/Repos/jasmin/compiler/syscall/jasmin_syscall.o jkem.o $<
+JASMIN_SOURCES := \
+  jpoly.jazz \
+  jpolyvec.jazz \
+  jfips203.jazz \
+  jindcpa.jazz \
+  jkem.jazz
 
-test/speed_indcpa: test/speed_indcpa.c $(HEADERS) $(SOURCES) jindcpa.o
-	$(CC) $(CFLAGS) -o $@ $(SOURCES) jindcpa.o $<
+JASMIN_ASSEMBLY := $(JASMIN_SOURCES:%.jazz=%.s)
 
-test/test_fips202: test/test_fips202.c $(HEADERS) $(SOURCES) jfips202.s
-	$(CC) $(CFLAGS) -o $@ $(SOURCES) jfips202.s $<
+# --
 
-test/test_poly_%: test/test_poly_%.c $(HEADERS) $(SOURCES) jpoly.s
-	$(CC) $(CFLAGS) -o $@ $(SOURCES) jpoly.s $<
+RANDOMBYTES := $(PROJECT_DIR)/jasmin/compiler/syscall/jasmin_syscall.o
 
-test/test_polyvec_%: test/test_polyvec_%.c $(HEADERS) $(SOURCES) jpolyvec.s
-	$(CC) $(CFLAGS) -o $@ $(SOURCES) jpolyvec.s $<
+$(RANDOMBYTES): $(PROJECT_DIR)/jasmin/compiler/syscall/jasmin_syscall.c $(PROJECT_DIR)/jasmin/compiler/syscall/jasmin_syscall.h
+	$(MAKE) -C $(@D)
 
+$(JASMIN_ASSEMBLY):
 %.s: %.jazz
-	$(JASMINC) -o $@ $(JFLAGS) $^ 
+	$(JASMINC) -nowarning -o $@ $(JFLAGS) $^ 
 
+#--
 
-.PHONY: ct clean
+compile-tests-poly: $(TESTS_POLY)
+$(TESTS_POLY):
+test/test_poly_%: test/test_poly_%.c $(HEADERS) $(C_SOURCES) jpoly.s
+	$(CC) $(CFLAGS) -o $@ $(C_SOURCES) jpoly.s $<
 
-ct:
-	$(JAZZCT) --infer jkem.jazz
+compile-tests-polyvec: $(TESTS_POLYVEC)
+$(TESTS_POLYVEC):
+test/test_polyvec_%: test/test_polyvec_%.c $(HEADERS) $(C_SOURCES) jpolyvec.s
+	$(CC) $(CFLAGS) -o $@ $(C_SOURCES) jpolyvec.s $<
+
+test/test_fips202: test/test_fips202.c $(HEADERS) $(C_SOURCES) jfips202.s
+	$(CC) $(CFLAGS) -o $@ $(C_SOURCES) jfips202.s $<
+
+test/test_indcpa: test/test_indcpa.c $(HEADERS) $(C_SOURCES) jindcpa.o
+	$(CC) $(CFLAGS) -o $@ $(C_SOURCES) jindcpa.o $<
+
+test/test_kem: test/test_kem.c $(HEADERS) $(C_SOURCES) $(RANDOMBYTES) jkem.o
+	$(CC) $(CFLAGS) -o $@ $(C_SOURCES) $(RANDOMBYTES) jkem.o $<
+
+compile-tests: test
+
+# --
+# note: to improve speed, remove for loop and define *.out targets
+
+run-tests-poly: compile-tests-poly
+	for i in $(TESTS_POLY); do ./$$i; done
+
+run-tests-polyvec: compile-tests-polyvec
+	for i in $(TESTS_POLYVEC); do ./$$i; done
+
+run-tests: compile-tests
+	for i in $(TESTS); do ./$$i; done
+
+#--
+
+test/speed_indcpa: test/speed_indcpa.c $(HEADERS) $(C_SOURCES) jindcpa.o
+	$(CC) $(CFLAGS) -o $@ $(C_SOURCES) jindcpa.o $<
+
+compile-speed: test/speed_indcpa
+
+run-speed: compile-speed
+	./test/speed_indcpa
+
+# --
+
+.PHONY: check-ct
+
+check-constant-time:
+	$(JASMIN_CT) --infer jkem.jazz
+
+# --
+
+.PHONY: clean
 
 clean:
 	-rm -f *.s
 	-rm -f jindcpa.o
 	-rm -f jkem.o
-	-rm -f test/test_poly_compress
-	-rm -f test/test_poly_decompress
-	-rm -f test/test_poly_tobytes
-	-rm -f test/test_poly_frombytes
-	-rm -f test/test_poly_tomsg
-	-rm -f test/test_poly_frommsg
-	-rm -f test/test_poly_add2
-	-rm -f test/test_poly_sub
-	-rm -f test/test_poly_ntt
-	-rm -f test/test_poly_invntt
-	-rm -f test/test_poly_basemul
-	-rm -f test/test_poly_frommont
-	-rm -f test/test_poly_reduce
-	-rm -f test/test_poly_csubq
-	-rm -f test/test_poly_getnoise
-	-rm -f test/test_polyvec_compress
-	-rm -f test/test_polyvec_decompress
-	-rm -f test/test_polyvec_tobytes
-	-rm -f test/test_polyvec_frombytes
-	-rm -f test/test_polyvec_add2
-	-rm -f test/test_polyvec_ntt
-	-rm -f test/test_polyvec_invntt
-	-rm -f test/test_polyvec_pointwise_acc
-	-rm -f test/test_polyvec_reduce
-	-rm -f test/test_polyvec_csubq
+	-rm -f $(TESTS_POLY)
+	-rm -f $(TESTS_POLYVEC)
 	-rm -f test/test_fips202
 	-rm -f test/test_indcpa
 	-rm -f test/test_kem
 	-rm -f test/speed_indcpa
 ifeq ($(OS),Darwin)
 	-rm -rf test/*.dSYM
 endif
+
+

code/jasmin/mlkem_ref/jpoly.jazz

@@ -7,9 +7,7 @@ export fn poly_compress_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_N] a;
-  stack u8[128] r;
 
   for i = 0 to MLKEM_N {
     t = (u16)[ap + 2*i];
@@ -23,9 +21,7 @@ export fn poly_decompress_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_N] r;
-  stack u8[128] a;
 
   r = _poly_decompress(r, ap);
 
@@ -39,7 +35,6 @@ export fn poly_tobytes_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_N] a;
 
   for i = 0 to MLKEM_N {
@@ -54,7 +49,6 @@ export fn poly_frombytes_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_N] r;
 
   r = _poly_frombytes(r, ap);
@@ -69,9 +63,7 @@ export fn poly_tomsg_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_N] a;
-  stack u8[32] r;
 
   for i = 0 to MLKEM_N {
     t = (u16)[ap + 2*i];
@@ -85,7 +77,6 @@ export fn poly_frommsg_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_N] r;
 
   r = _poly_frommsg(r, ap);

code/jasmin/mlkem_ref/jpolyvec.jazz

@@ -7,7 +7,6 @@ export fn polyvec_tobytes_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_VECN] a;
 
   for i = 0 to MLKEM_VECN {
@@ -23,7 +22,6 @@ export fn polyvec_decompress_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_VECN] r;
 
   r = __polyvec_decompress(ap);
@@ -39,7 +37,6 @@ export fn polyvec_compress_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_VECN] a;
 
   for i = 0 to MLKEM_VECN {
@@ -55,7 +52,6 @@ export fn polyvec_frombytes_jazz(reg u64 rp, reg u64 ap)
 {
   inline int i;
   reg u16 t;
-  reg u8 c;
   stack u16[MLKEM_VECN] r;
 
   r = __polyvec_frombytes(ap);