Makefile
all: verify extract test
# Old targets, backwards-compat:
.PHONY: old-%
old-%:
$(MAKE) -f Makefile.old $*
# 0. Paths and includes
HACL_HOME ?= ..
HASH_DIR=$(HACL_HOME)/code/hash-new
ROOTS=$(addprefix $(HASH_DIR)/Hacl.Hash.,MD5.fst SHA1.fst SHA2.fst)
ALL_CHECKED_FILES = $(addsuffix .checked,$(ROOTS))
.depend:
@$(FSTAR) --dep full $(ROOTS) --extract '* -Prims -FStar +FStar.Endianness +FStar.Kremlin.Endianness' > $@
include .depend
include Makefile.common
# 1. Top-level entry points for this Makefile
verify: $(ALL_CHECKED_FILES)
extract: dist/compact/Makefile.include dist/generic/Makefile.include
# Backwards compat target name
extract-c: extract old-extract-c
clean: clean-c
find $(DIRS) -iname '*.checked' | xargs rm -rf
clean-c: old-clean-c
rm -rf $(OUTPUT_DIR)
test:
# 2. Verification
%.checked:
$(FSTAR) $< && \
touch $@
# 3. Extraction. Note that all the C files are prefixed with Hacl_. Cleaner!
.PRECIOUS: %.krml
$(OUTPUT_DIR)/%.krml:
$(FSTAR) --codegen Kremlin \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
$(notdir $(subst .checked,,$<)) && \
touch $@
dist/compact/Makefile.include: \
EXTRA=-bundle Hacl.Hash.MD5+Hacl.Hash.Core.MD5+Hacl.Hash.SHA1+Hacl.Hash.Core.SHA1+Hacl.Hash.SHA2+Hacl.Hash.Core.SHA2+Hacl.Hash.Core.SHA2.Constants=Hacl.Hash.*[rename=Hacl_Hash] \
-bundle Prims \
-bundle LowStar.* \
-bundle C,C.Loops,Spec.Loops,C.Endianness,FStar.*[rename=Hacl_Kremlib] \
-minimal \
-add-include '"kremlin/internal/types.h"' \
-add-include '"kremlin/c_endianness.h"' \
-add-include '<string.h>' \
-fparentheses -fno-shadow -fcurly-braces
# For the time being, we rely on the old extraction to give us self-contained
# files
HACL_OLD_FILES=\
curve25519/x25519-c/Hacl_Curve25519.c \
ed25519/ed25519-c/Hacl_Ed25519.c \
salsa-family/chacha-c/Hacl_Chacha20.c \
poly1305/poly-c/AEAD_Poly1305_64.c \
poly1305/poly-c/Hacl_Poly1305_64.c \
api/aead-c/Hacl_Chacha20Poly1305.c
dist/%/Makefile.include: $(ALL_KRML_FILES) | old-extract-c
mkdir -p $(dir $@)
cp $(HACL_OLD_FILES) $(patsubst %.c,%.h,$(HACL_OLD_FILES)) $(dir $@)
$(KRML) $(EXTRA) -tmpdir $(dir $@) -skip-compilation \
-bundle Spec.*[rename=Hacl_Spec] $^ \
-warn-error @4