include $(HACL_HOME)/Makefile.include


FSTAR_INCLUDES = \
	--include $(KREMLIN_HOME)/kremlib \
	--include $(HACL_HOME)/lib \
	--include $(HACL_HOME)/specs \
	--include $(HACL_HOME)/specs/lemmas

#
# HACL Library files
#

KREMLIN_LIBS = Spec.Loops.fst
KREMLIN_LIBS_ML = Spec_Loops.ml
KREMLIN_LIBS_FILES = $(addprefix $(KREMLIN_HOME)/kremlib/, $(KREMLIN_LIBS))
KREMLIN_LIBS_MODULES = $(KREMLIN_LIBS:.fst=)
KREMLIN_LIBS_EX = $(addprefix --extract_module , $(KREMLIN_LIBS:.fst=))

LIBS = Lib.Result.fst Lib.NatMod.fst Lib.IntTypes.fst Lib.RawIntTypes.fst Lib.LoopCombinators.fst Lib.Sequence.fst Lib.ByteSequence.fst Lib.PrintSequence.fst Lib.Network.fst
LIBS_ML = Lib_Result.ml Lib_NatMod.ml Lib_IntTypes.ml Lib_RawIntTypes.ml Lib_LoopCombinators.ml Lib_Sequence.ml Lib_ByteSequence.ml Lib_PrintSequence.ml Lib_Network.ml
LIBS_FILES = $(addprefix $(HACL_HOME)/lib/, $(LIBS))
LIBS_MODULES = $(LIBS:.fst=)
LIBS_EX = $(addprefix --extract_module , $(LIBS:.fst=))

#
# HACL Crypto files
#

HACL = Spec.Curve25519.fst Spec.Curve448.fst Spec.SHA2.Constants.fst Spec.Hash.Definitions.fst Spec.Hash.PadFinish.fst Spec.MD5.fst Spec.SHA1.fst Spec.SHA2.fst Spec.Hash.fst Spec.Hash.Incremental.fst Spec.Agile.Hash.fst Spec.Agile.HMAC.fst Spec.Agile.HKDF.fst Spec.GaloisField.fst Spec.AES.fst Spec.GF128.fst Spec.AES_GCM.fst Spec.Chacha20.fst Spec.Poly1305.fst Spec.Chacha20Poly1305.fst Spec.Agile.AEAD.fst Spec.Agile.DH.fst Spec.HPKE.fst Spec.Ed25519.fst

HACL_ML = Spec_Curve25519.ml Spec_Curve448.ml Spec_SHA2_Constants.ml Spec_Hash_Definitions.ml Spec_Hash_PadFinish.ml Spec_MD5.ml Spec_SHA1.ml Spec_SHA2.ml Spec_Hash.ml Spec_Hash_Incremental.ml Spec_Agile_Hash.ml Spec_Agile_HMAC.ml Spec_Agile_HKDF.ml Spec_GaloisField.ml Spec_AES.ml Spec_GF128.ml Spec_AES_GCM.ml Spec_Chacha20.ml Spec_Poly1305.ml Spec_Chacha20Poly1305.ml Spec_Agile_AEAD.ml Spec_Agile_DH.ml Spec_HPKE.ml Spec_Ed25519.ml


HACL_FILES = $(addprefix $(HACL_HOME)/specs/, $(HACL))
HACL_MODULES = $(HACL:.fst=)


all: build/ml/libhacl.cmxa

build/ml/libhacl.cmxa: $(KREMLIN_LIBS_FILES) $(LIBS_FILES) $(HACL_FILES)
	mkdir -p build/ml
	cp $(HACL_HOME)/lib/ml/Lib_RandomSequence.ml build/ml
	$(FSTAR) --codegen OCaml --lax --expose_interfaces \
		$(addprefix --extract_module , $(KREMLIN_LIBS_MODULES)) \
		$(addprefix --extract_module , $(LIBS_MODULES)) \
		$(addprefix --extract_module , $(HACL_MODULES)) \
		--odir build/ml $^
	OCAMLPATH="$(FSTAR_HOME)/bin" ocamlfind opt -a -g -linkall -thread -w -20-26-3-8-58 \
		-package fstarlib -package batteries,zarith,stdint,cryptokit -I build/ml \
		$(addprefix build/ml/, $(KREMLIN_LIBS_ML)) \
		$(addprefix build/ml/, $(LIBS_ML)) \
		build/ml/Lib_RandomSequence.ml \
		$(addprefix build/ml/, $(HACL_ML)) \
		-o build/ml/libhacl.cmxa

clean:
	rm -rf *~ *.exe build/ml