Makefile

# Top-level entry points.  See README.md.
#
#   make [-j]          compile the 13 Jasmin units to assembly and build the
#                      shared libraries (and the v1.1 C baseline)
#   make tests         functional tests against the C implementations
#   make kats          replay the official known-answer tests (new spec)
#   make check-ct      constant-time check of the KEM exports (jasmin-ct)
#   make check-sct     speculative constant-time check (jasmin-ct --sct)
#   make check-ec      re-check the EasyCrypt specification and proofs
#   make extract       extract the reference codec to EasyCrypt and type-check
#   make headers       regenerate include/*.h from the Jasmin export signatures
#   make check-headers fail if include/*.h are stale
#   make bench         build the benchmark harnesses and time the KEM operations
#                      (BENCH_GROUPS="kem pke" for more, BENCH_GROUPS=all for everything)
#   make bench-run     full run of every harness, results + provenance in src/bench/results/
#   make memcheck      valgrind memcheck over the functional tests (SHAKE family)
#   make clean
#
# Knobs are documented in Makefile.conf (JASMINC, CC, OPENSSLDIR, ...).

include Makefile.conf

JOBS ?= $(shell nproc 2>/dev/null || echo 2)
# SMT timeout (seconds) for check-ec; easycrypt.project says 2, which is
# enough on an idle machine but flaky on loaded CI runners
EC_TIMEOUT ?= 10

NEW  := src/scloudplus_jasmin_opt
REF  := src/scloudplus_jasmin_ref
V11  := src/scloud11_jasmin_opt
CREF := src/scloud11_cref

.DEFAULT_GOAL := all

all: new ref v11 cref

new:
	$(MAKE) -C $(NEW) all
ref:
	$(MAKE) -C $(REF) all
v11:
	$(MAKE) -C $(V11) all
cref:
	$(MAKE) -C $(CREF) all

# ---- tests ---------------------------------------------------------------
tests: tests-new tests-ref tests-v11

tests-new:
	$(MAKE) -C $(NEW)/tests run-tests
tests-ref:
	$(MAKE) -C $(REF)/tests run-tests
tests-v11:
	$(MAKE) -C $(V11)/tests run-tests
tests-cref:
	$(MAKE) -C $(CREF) tests

kats:
	$(MAKE) -C $(NEW)/tests run-kats

# ---- leakage checks --------------------------------------------------------
check-ct:
	$(MAKE) -C $(NEW) check-ct
	$(MAKE) -C $(V11) check-ct

check-sct:
	$(MAKE) -C $(NEW) check-sct
	$(MAKE) -C $(V11) check-sct

# ---- EasyCrypt -------------------------------------------------------------
# easycrypt needs a why3 prover configuration once per user
EC_WHY3CONF := $(HOME)/.config/easycrypt/why3.conf
$(EC_WHY3CONF):
	$(EASYCRYPT) why3config

# the extracted models are produced first: the proofs do not import them
# yet, but the implementation-correctness proofs (D2.1, Section 6) will
extract: $(EC_WHY3CONF)
	$(MAKE) -C proof/extraction check

check-ec: $(EC_WHY3CONF) extract
	$(EASYCRYPT) runtest -jobs $(JOBS) -timeout $(EC_TIMEOUT) config/tests.config spec

# ---- headers ---------------------------------------------------------------
headers:
	python3 scripts/gen-headers.py include

# regenerate into a scratch directory and compare header by header
check-headers:
	@tmp=$$(mktemp -d) && python3 scripts/gen-headers.py $$tmp >/dev/null && stale=0; \
	for f in $$tmp/*.h; do \
	  h=include/$$(basename $$f); \
	  if [ ! -f $$h ]; then echo "  MISSING  $$h"; stale=1; \
	  elif diff -u $$h $$f >$$tmp/diff; then echo "  OK       $$h"; \
	  else echo "  STALE    $$h"; sed 's/^/           /' $$tmp/diff; stale=1; fi; \
	done; \
	for h in include/*.h; do [ -f $$tmp/$$(basename $$h) ] || { echo "  EXTRA    $$h (no export root generates it)"; stale=1; }; done; \
	rm -rf $$tmp; \
	if [ $$stale -ne 0 ]; then echo "check-headers: include/ is stale, run 'make headers'"; exit 1; \
	else echo "check-headers: all headers match the export signatures"; fi

# ---- benchmarks ------------------------------------------------------------
BENCH_BINS := $(foreach l,$(LEVELS_V11),scloud11_bench_$(l) funs11_bench_$(l)) \
              $(foreach l,$(LEVELS_NEW),scloud_bench_$(l)_aes scloud_bench_$(l)_shake \
                                        funs_bench_ref_$(l) funs_bench_opt_$(l))
# groups timed by `make bench` (kem, pke, sample, matrix, pack, hash, encode; all)
BENCH_GROUPS ?= kem

bench:
	$(MAKE) -C src/bench all
	@missing=0; for b in $(BENCH_BINS); do [ -x src/bench/$$b ] || { echo "  MISSING src/bench/$$b"; missing=1; }; done; \
	[ $$missing -eq 0 ] || exit 1; \
	echo; echo "$$(echo $(BENCH_BINS) | wc -w) harnesses built; timing groups: $(BENCH_GROUPS)"; echo
	scripts/bench.sh $(BENCH_GROUPS)

bench-run:
	scripts/run-bench.sh

# ---- valgrind memcheck -----------------------------------------------------
# stage tests of every level plus the SHAKE-family matrix/pke/kem tests
# (valgrind does not emulate VAES; the AES family joins when the tree is
# built with USE_VAES = false).  MEMCHECK_KATS=1 also replays the KATs.
MEMCHECK_TESTS := $(foreach l,$(LEVELS_NEW),encode_test_$(l) hash_test_$(l) pack_test_$(l) sample_test_$(l) \
                    matrix_test_$(l)_shake pke_test_$(l)_shake kem_test_$(l)_shake kat_test_$(l)_shake)

memcheck:
	$(MAKE) -C $(NEW)/tests $(MEMCHECK_TESTS)
	scripts/memcheck.sh

# ---- housekeeping ----------------------------------------------------------
clean:
	$(MAKE) -C $(NEW) clean
	$(MAKE) -C $(REF) clean
	$(MAKE) -C $(V11) clean
	$(MAKE) -C $(CREF) clean
	$(MAKE) -C src/bench clean
	$(MAKE) -C proof/extraction clean
	$(MAKE) -C spec clean

.PHONY: all new ref v11 cref tests tests-new tests-ref tests-v11 tests-cref kats \
        check-ct check-sct check-ec extract headers check-headers bench bench-run \
        memcheck clean