Refactor Build System for Easier Extensibility and Future Optimizations

.github/workflows/bench.yml

@@ -16,13 +16,13 @@ jobs:
        target:
         - system: rpi4
           name: Arm Cortex-A72 (Raspberry Pi 4) benchmarks
-          cmd: tests bench -c PMU --cflags -mcpu=cortex-a72 -v --output output.json
+          cmd: tests bench -c PMU --arch-flags -mcpu=cortex-a72 -v --output output.json
         - system: rpi5
           name: Arm Cortex-A76 (Raspberry Pi 5) benchmarks
-          cmd: tests bench -c PERF --cflags -mcpu=cortex-a76 --arch-flags -march=armv8.2-a -v --output output.json
+          cmd: tests bench -c PERF --arch-flags "-mcpu=cortex-a76 -march=armv8.2-a" -v --output output.json
         - system: a55
           name: Arm Cortex-A55 (Snapdragon 888) benchmarks
-          cmd: tests bench -c PERF --cflags "-static -mcpu=cortex-a55" --arch-flags -march=armv8.2-a -w exec-on-a55 -v --output output.json
+          cmd: tests bench -c PERF --cflags -static --arch-flags "-mcpu=cortex-a55 -march=armv8.2-a" -w exec-on-a55 -v --output output.json
     runs-on: self-hosted-${{ matrix.target.system }}
     defaults:
       run:

.gitignore

@@ -4,5 +4,4 @@
 .direnv
 .vscode
 .idea
-test/bin/
-test/obj/
+test/build

Makefile

@@ -6,106 +6,32 @@
 all: mlkem bench kat nistkat
 
 include mk/config.mk
+include mk/crypto.mk
+include mk/schemes.mk
+include mk/hal.mk
+include mk/rules.mk
 
-INCLUDE_RANDOM = -I randombytes
-INCLUDE_NISTRANDOM = -I test/nistrng
-
-CFLAGS_RANDOMBYTES = ${CFLAGS} ${INCLUDE_RANDOM}
-CFLAGS_NISTRANDOMBYTES = ${CFLAGS} ${INCLUDE_NISTRANDOM}
-NISTFLAGS += -Wno-unused-result -O3 -fomit-frame-pointer
-RM = /bin/rm
-
-SOURCES = mlkem/kem.c mlkem/indcpa.c mlkem/polyvec.c mlkem/poly.c mlkem/ntt.c mlkem/cbd.c mlkem/reduce.c mlkem/verify.c
-SOURCESKECCAK = $(SOURCES) fips202/keccakf1600.c fips202/fips202.c fips202/fips202x4.c mlkem/symmetric-shake.c
-SOURCESKECCAKRANDOM = $(SOURCESKECCAK) randombytes/randombytes.c
-SOURCESNISTKATS = $(SOURCESKECCAK) test/nistrng/aes.c test/nistrng/rng.c
-SOURCESBENCH = $(SOURCESKECCAKRANDOM) test/hal.c
-
-HEADERS = mlkem/params.h mlkem/kem.h mlkem/indcpa.h mlkem/polyvec.h mlkem/poly.h mlkem/ntt.h mlkem/cbd.h mlkem/reduce.c mlkem/verify.h mlkem/symmetric.h
-HEADERSKECCAK = $(HEADERS) fips202/keccakf1600.h fips202/fips202.h fips202/fips202x4.h
-HEADERSKECCAKRANDOM = $(HEADERSKECCAK) randombytes/randombytes.h
-HEADERNISTKATS = $(HEADERSKECCAK) test/nistrng/aes.h test/nistrng/randombytes.h
-HEADERSBENCH = $(HEADERSKECCAKRANDOM) test/hal.h
+MAKEFLAGS = --no-print-directory
 
 mlkem: \
-  test/bin/test_kyber512 \
-  test/bin/test_kyber768 \
-  test/bin/test_kyber1024
+  $(MLKEM512_DIR)/bin/test_kyber512 \
+  $(MLKEM768_DIR)/bin/test_kyber768 \
+  $(MLKEM1024_DIR)/bin/test_kyber1024 \
 
-bench: \
-  test/bin/bench_kyber512 \
-  test/bin/bench_kyber768 \
-  test/bin/bench_kyber1024
+bench:
+	$(MAKE) $(MAKEFLAGS) BENCH=1 $(MLKEM512_DIR)/bin/bench_kyber512
+	$(MAKE) $(MAKEFLAGS) BENCH=1 $(MLKEM768_DIR)/bin/bench_kyber768
+	$(MAKE) $(MAKEFLAGS) BENCH=1 $(MLKEM1024_DIR)/bin/bench_kyber1024
 
-nistkat: \
-  test/bin/gen_NISTKAT512 \
-  test/bin/gen_NISTKAT768 \
-  test/bin/gen_NISTKAT1024
+nistkat:
+	$(MAKE) $(MAKEFLAGS) RNG=NISTRNG $(MLKEM512_DIR)/bin/gen_NISTKAT512
+	$(MAKE) $(MAKEFLAGS) RNG=NISTRNG $(MLKEM768_DIR)/bin/gen_NISTKAT768
+	$(MAKE) $(MAKEFLAGS) RNG=NISTRNG $(MLKEM1024_DIR)/bin/gen_NISTKAT1024
 
 kat: \
-  test/bin/gen_KAT512 \
-  test/bin/gen_KAT768 \
-  test/bin/gen_KAT1024
-
-test/bin/test_kyber512: test/test_kyber.c $(SOURCESKECCAKRANDOM) $(HEADERSKECCAKRANDOM) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=2 $(SOURCESKECCAKRANDOM) $< -o $@
-
-test/bin/test_kyber768: test/test_kyber.c $(SOURCESKECCAKRANDOM) $(HEADERSKECCAKRANDOM) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=3 $(SOURCESKECCAKRANDOM) $< -o $@
-
-test/bin/test_kyber1024: test/test_kyber.c $(SOURCESKECCAKRANDOM) $(HEADERSKECCAKRANDOM) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=4 $(SOURCESKECCAKRANDOM) $< -o $@
-
-test/bin/bench_kyber512: test/bench_kyber.c $(SOURCESBENCH) $(HEADERSBENCH) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=2 $(SOURCESBENCH) $< -o $@
-
-test/bin/bench_kyber768: test/bench_kyber.c $(SOURCESBENCH) $(HEADERSBENCH) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=3 $(SOURCESBENCH) $< -o $@
-
-test/bin/bench_kyber1024: test/bench_kyber.c $(SOURCESBENCH) $(HEADERSBENCH) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=4 $(SOURCESBENCH) $< -o $@
-
-test/bin/gen_KAT512: test/gen_KAT.c $(SOURCESKECCAKRANDOM) $(HEADERSKECCAKRANDOM) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=2 $(SOURCESKECCAKRANDOM) $< -o $@
-
-test/bin/gen_KAT768: test/gen_KAT.c $(SOURCESKECCAKRANDOM) $(HEADERSKECCAKRANDOM) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=3 $(SOURCESKECCAKRANDOM) $< -o $@
-
-test/bin/gen_KAT1024: test/gen_KAT.c $(SOURCESKECCAKRANDOM) $(HEADERSKECCAKRANDOM) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_RANDOMBYTES) -DKYBER_K=4 $(SOURCESKECCAKRANDOM) $< -o $@
-
-test/bin/gen_NISTKAT512: test/gen_NISTKAT.c $(SOURCESNISTKATS) $(HEADERNISTKATS) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_NISTRANDOMBYTES) -DKYBER_K=2 $(SOURCESNISTKATS) $< -o $@
-
-test/bin/gen_NISTKAT768: test/gen_NISTKAT.c $(SOURCESNISTKATS) $(HEADERNISTKATS) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_NISTRANDOMBYTES) -DKYBER_K=3 $(SOURCESNISTKATS) $< -o $@
-
-test/bin/gen_NISTKAT1024: test/gen_NISTKAT.c $(SOURCESNISTKATS) $(HEADERNISTKATS) $(CONFIG)
-	$(Q)echo "  CC      $@"
-	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
-	$(CC) $(CFLAGS_NISTRANDOMBYTES) -DKYBER_K=4 $(SOURCESNISTKATS) $< -o $@
+  $(MLKEM512_DIR)/bin/gen_KAT512 \
+  $(MLKEM768_DIR)/bin/gen_KAT768 \
+  $(MLKEM1024_DIR)/bin/gen_KAT1024
 
 # emulate ARM64 binary on x86_64 machine
 emulate:
@@ -114,5 +40,4 @@ emulate:
 
 clean:
 	-$(RM) -rf *.gcno *.gcda *.lcov *.o *.so
-	-$(RM) -rf test/bin
-	-$(RM) -rf test/obj
+	-$(RM) -rf $(BUILD_DIR)

cbmc/litani.nix

@@ -4,7 +4,7 @@
 , fetchFromGitHub
 }:
 
-stdenvNoCC.mkDerivation rec {
+stdenvNoCC.mkDerivation {
   pname = "litani";
   version = "8002c240ef4f424039ed3cc32e076c0234d01768";
   src = fetchFromGitHub {

mk/config.mk

@@ -7,7 +7,7 @@ SRCDIR := $(CURDIR)
 ##############
 # GCC config #
 ##############
-CROSS_PREFIX ?= 
+CROSS_PREFIX ?=
 CC := $(CROSS_PREFIX)gcc
 CPP := $(CROSS_PREFIX)cpp
 AR := $(CROSS_PREFIX)ar
@@ -32,10 +32,13 @@ CFLAGS += \
 	-O3 \
 	-fomit-frame-pointer \
 	-pedantic \
+	-MMD \
 	-I mlkem \
 	-I fips202 \
 	$(CPPFLAGS)
 
+LINKDEPS += $(LIBDEPS)
+
 ##################
 # Some Variables #
 ##################
@@ -65,9 +68,16 @@ endif
 # Include retained variables #
 ##############################
 
-RETAINED_VARS :=
+RNG ?=
+RETAINED_VARS := RNG BENCH CYCLES
+
+BUILD_DIR := test/build
+LIB_DIR := $(BUILD_DIR)/lib
 
-CONFIG := test/obj/.config.mk
+MAKE_OBJS = $(2:%=$(1)/%.o)
+OBJS = $(call MAKE_OBJS,$(BUILD_DIR),$(1))
+
+CONFIG := $(BUILD_DIR)/config.mk
 
 -include $(CONFIG)
 
@@ -77,8 +87,6 @@ $(CONFIG):
 	@echo "# These variables are retained and can't be changed without a clean" > $@
 	@$(foreach var,$(RETAINED_VARS),echo "$(var) := $($(var))" >> $@; echo "LAST_$(var) := $($(var))" >> $@;)
 
-RETAINED_VARS += CYCLES
-
 define VAR_CHECK
 ifneq ($$(origin LAST_$(1)),undefined)
 ifneq "$$($(1))" "$$(LAST_$(1))"

mk/crypto.mk

@@ -0,0 +1,23 @@
+# SPDX-License-Identifier: Apache-2.0
+LDLIBS += -L$(LIB_DIR)
+
+LIBDEPS += $(LIB_DIR)/libfips202.a
+LDLIBS += -lfips202
+CPPFLAGS += -Ifips202
+
+ifeq ($(RNG),NISTRNG)
+	LIBDEPS += $(LIB_DIR)/libnistrng.a
+	LDLIBS += -lnistrng
+	CPPFLAGS += -Itest/nistrng
+else
+	LIBDEPS += $(LIB_DIR)/librng.a
+	LDLIBS += -lrng
+	CPPFLAGS += -Irandombytes
+endif
+
+$(LIB_DIR)/librng.a: $(call OBJS,$(wildcard randombytes/*.c))
+
+$(LIB_DIR)/libnistrng.a: CFLAGS += -Wno-unused-result -O3 -fomit-frame-pointer
+$(LIB_DIR)/libnistrng.a: $(call OBJS,$(wildcard test/nistrng/*.c))
+
+$(LIB_DIR)/libfips202.a: $(call OBJS,$(wildcard fips202/*.c))

mk/hal.mk

@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: Apache-2.0
+ifdef BENCH
+
+LIBDEPS += $(LIB_DIR)/libhal.a
+LDLIBS += -lhal
+CPPFLAGS += -Itest/hal
+$(LIB_DIR)/libhal.a: $(call OBJS,$(wildcard test/hal/*.c))
+
+endif

mk/rules.mk

@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: Apache-2.0
+$(BUILD_DIR)/%: $(LINKDEPS) $(CONFIG)
+	$(Q)echo "  LD      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(LD) $(CFLAGS) -o $@ $(filter %.o,$^) $(LDLIBS)
+
+$(LIB_DIR)/%.a: $(CONFIG)
+	$(Q)echo "  AR      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)rm -f $@
+	$(Q)$(AR) rcs $@ $(filter %.o,$^)
+
+$(BUILD_DIR)/%.c.o: %.c $(CONFIG)
+	$(Q)echo "  CC      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)$(CC) -c -o $@ $(CFLAGS) $<
+
+$(BUILD_DIR)/mlkem512/%.c.o: %.c $(CONFIG)
+	$(Q)echo "  CC      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)$(CC) -c -o $@ $(CFLAGS) $<
+
+$(BUILD_DIR)/mlkem512/%.S.o: %.S $(CONFIG)
+	$(Q)echo "  AS      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)$(CC) -c -o $@ $(CFLAGS) $<
+
+$(BUILD_DIR)/mlkem768/%.c.o: %.c $(CONFIG)
+	$(Q)echo "  CC      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)$(CC) -c -o $@ $(CFLAGS) $<
+
+$(BUILD_DIR)/mlkem768/%.S.o: %.S $(CONFIG)
+	$(Q)echo "  AS      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)$(CC) -c -o $@ $(CFLAGS) $<
+
+$(BUILD_DIR)/mlkem1024/%.c.o: %.c $(CONFIG)
+	$(Q)echo "  CC      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)$(CC) -c -o $@ $(CFLAGS) $<
+
+$(BUILD_DIR)/mlkem1024/%.S.o: %.S $(CONFIG)
+	$(Q)echo "  AS      $@"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(Q)$(CC) -c -o $@ $(CFLAGS) $<

mk/schemes.mk

@@ -0,0 +1,18 @@
+# SPDX-License-Identifier: Apache-2.0
+SOURCES = $(wildcard mlkem/*.c)
+
+CPPFLAGS += -Imlkem
+TESTS = test_kyber bench_kyber gen_NISTKAT gen_KAT
+
+MLKEM512_DIR = $(BUILD_DIR)/mlkem512
+MLKEM768_DIR = $(BUILD_DIR)/mlkem768
+MLKEM1024_DIR = $(BUILD_DIR)/mlkem1024
+
+$(MLKEM512_DIR)/bin/%: CPPFLAGS += -DKYBER_K=2
+$(TESTS:%=$(MLKEM512_DIR)/bin/%512):$(MLKEM512_DIR)/bin/%512: $(MLKEM512_DIR)/test/%.c.o $(call MAKE_OBJS,$(MLKEM512_DIR),$(SOURCES))
+
+$(MLKEM768_DIR)/bin/%: CPPFLAGS += -DKYBER_K=3
+$(TESTS:%=$(MLKEM768_DIR)/bin/%768):$(MLKEM768_DIR)/bin/%768: $(MLKEM768_DIR)/test/%.c.o $(call MAKE_OBJS,$(MLKEM768_DIR),$(SOURCES))
+
+$(MLKEM1024_DIR)/bin/%: CPPFLAGS += -DKYBER_K=4
+$(TESTS:%=$(MLKEM1024_DIR)/bin/%1024):$(MLKEM1024_DIR)/bin/%1024: $(MLKEM1024_DIR)/test/%.c.o  $(call MAKE_OBJS,$(MLKEM1024_DIR),$(SOURCES))