# Dark Factory verifier kit — Makefile.
#
# Runs gnatprove --level=1 on each routine in routines/ and produces
# a summary that should match expected-results.txt line for line.
#
# Usage:
#   make ROUTINE=<routine>        run gnatprove on one routine
#   make all                       run gnatprove on every routine
#   make clean                     remove generated artefacts
#
# Requires:
#   gnatprove   (AdaCore SPARK Pro / Community 2024 / GNAT 13+)
#   gprbuild    (bundled with GNAT)

# All routines this kit contains.
ROUTINES = \
	blas-ddot \
	blas-daxpy \
	blas-dscal \
	blas-dnrm2 \
	blas-dgemv \
	blas-dgemm \
	fftpack-cfftf \
	lapack-dpotrf \
	lapack-dgeqrf \
	lapack-dgetrf \
	phase3-relu \
	phase3-max_pool \
	phase3-layernorm \
	phase3-conv2d_fp64 \
	phase3-int8-matmul

GNATPROVE = gnatprove
LEVEL     ?= 1

# Pick the SPARK lemma library if available — improves discharge on
# loop invariants and recursive ghosts.
SPARKLIB_OBJ ?= obj/sparklib

.PHONY: all clean help one $(ROUTINES)

help:
	@echo "Dark Factory verifier kit"
	@echo ""
	@echo "Usage:"
	@echo "  make ROUTINE=<name>    run gnatprove on one routine"
	@echo "  make all               run gnatprove on every routine"
	@echo "  make clean             remove obj/ and actual-results.txt"
	@echo ""
	@echo "Routines: $(ROUTINES)"

# Run one routine, named via ROUTINE=...
one:
	@if [ -z "$(ROUTINE)" ]; then echo "ERROR: set ROUTINE=<name>"; exit 1; fi
	@if [ ! -d "routines/$(ROUTINE)" ]; then echo "ERROR: no such routine $(ROUTINE)"; exit 1; fi
	@echo "=== $(ROUTINE) ==="
	@cd routines/$(ROUTINE) && $(GNATPROVE) -P build.gpr --level=$(LEVEL) --output=oneline -XSPARKLIB_OBJECT_DIR=$(SPARKLIB_OBJ) 2>&1 || true
	@cd routines/$(ROUTINE) && grep -E '^Total' obj/gnatprove/gnatprove.out | head -1

# Run all routines and write a summary table to actual-results.txt.
all:
	@echo "Running gnatprove --level=$(LEVEL) on $(words $(ROUTINES)) routines..."
	@: > actual-results.txt
	@printf "%-22s %10s %10s %12s\n" "routine" "obligations" "unproved" "discharge%%" | tee -a actual-results.txt
	@printf "%-22s %10s %10s %12s\n" "---" "---" "---" "---" | tee -a actual-results.txt
	@for r in $(ROUTINES); do \
		echo "[$$r]"; \
		cd routines/$$r && \
		$(GNATPROVE) -P build.gpr --level=$(LEVEL) --output=oneline -XSPARKLIB_OBJECT_DIR=$(SPARKLIB_OBJ) >/dev/null 2>&1 || true; \
		total=$$(grep -E '^Total' obj/gnatprove/gnatprove.out | awk '{print $$2}'); \
		unproved=$$(grep -E '^Total' obj/gnatprove/gnatprove.out | grep -oE '[0-9]+ \([0-9]+%\)$$' | awk '{print $$1}'); \
		[ -z "$$total" ] && total=0; \
		[ -z "$$unproved" ] && unproved=0; \
		discharged=$$((total - unproved)); \
		pct=$$(awk "BEGIN{if ($$total>0) printf \"%.1f\", ($$discharged/$$total)*100; else print \"0.0\"}"); \
		cd ../..; \
		printf "%-22s %10d %10d %11s%%\n" "$$r" "$$total" "$$unproved" "$$pct" | tee -a actual-results.txt; \
	done
	@echo ""
	@echo "Compare against the published numbers:"
	@echo "  diff expected-results.txt actual-results.txt"

clean:
	@for r in $(ROUTINES); do \
		rm -rf routines/$$r/obj routines/$$r/*.ali; \
	done
	@rm -f actual-results.txt
	@echo "cleaned."