Makefile.common

# This Makefile can be safely included from sub-directories for the purposes of
# defining the .fst-in targets, as long as the sub-directory defines HACL_HOME.

# Define a newline variable for error messages.
# The two empty lines are needed.
define newline


endef

ifndef HACL_HOME
HACL_HOME 	:= $(shell pwd)
endif

# Put your local configuration (e.g. HACL_HOME, KRML_HOME, etc.) in
# Makefile.config
-include $(HACL_HOME)/Makefile.config

# Essentially FSTAR_EXE ?= fstar.exe, but we want to
# 1) Make it absolute
# 2) Fail early if not found
ifndef FSTAR_EXE
FSTAR_EXE := $(shell which fstar.exe)
ifneq ($(.SHELLSTATUS),0)
  $(error "Did not find F* in PATH, add it or set FSTAR_EXE")
endif
endif

ifndef KRML_HOME
# assuming an Everest source tree
KRML_HOME 	:= $(HACL_HOME)/../karamel
endif

# Check that the relevant homes and executables at least exist.
mustexist =						\
  $(if $(wildcard $(value $(strip $1))),,		\
    $(error $1 ($(value $(strip $1))) does not exist))

# eval $(FSTAR_OCAMLENV) extends the environment so we can
# find fstar's ocaml libraries.
FSTAR_OCAMLENV := $(shell $(FSTAR_EXE) --ocamlenv)

# We also extend this variable to reduce warnings.
FSTAR_OCAMLENV += OCAMLFIND_IGNORE_DUPS_IN='$(shell ocamlc -where)/compiler-libs:$(OCAMLFIND_IGNORE_DUPS_IN)';
FSTAR_OCAMLENV += export OCAMLFIND_IGNORE_DUPS_IN;

$(call mustexist, FSTAR_EXE)
$(call mustexist, KRML_HOME)

# Find the location of the checked files in F*'s library, for the
# vale-depend call. Note: we still rely on the fact this directory is
# flat.
FSTAR_ULIB_CHECKED := $(dir $(shell $(FSTAR_EXE) --locate_file Prims.fst.checked))

ifndef VALE_HOME
# assuming an Everest source tree
VALE_HOME	:= $(HACL_HOME)/../vale
endif

# Make all paths absolute, so that `make` only sees a single view of
# each file name, especially when generating dependency trees. On
# Cygwin, we additionally need to use Windows paths instead of Cygwin
# paths.

ifeq ($(OS),Windows_NT)
  maybe_cygpath=$(shell cygpath -m $(1))
else
  maybe_cygpath=$(1)
endif

sanitize_path=$(call maybe_cygpath,$(realpath $(1)))

HACL_HOME := $(call sanitize_path,$(HACL_HOME))
KRML_HOME := $(call sanitize_path,$(KRML_HOME))
FSTAR_ULIB_CHECKED := $(call sanitize_path,$(FSTAR_ULIB_CHECKED))
VALE_HOME := $(call sanitize_path,$(VALE_HOME))

include $(HACL_HOME)/Makefile.include

# $(FSTAR_ULIB_CHECKED) necessary for vale-depend
INCLUDES = \
  $(ALL_HACL_DIRS) \
  $(FSTAR_ULIB_CHECKED) \
  $(KRML_HOME)/krmllib/obj \
  $(KRML_HOME)/krmllib

# 0. Vale

# Please keep this in sync with vale/Hacl.Vale.fst.config.json
# so the vscode extension works seamlessly.
VALE_FSTAR_FLAGS=--z3cliopt smt.arith.nl=false \
  --z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 \
  --max_fuel 1 --max_ifuel 1 --initial_ifuel 0 \
  --smtencoding.elim_box true --smtencoding.l_arith_repr native \
  --smtencoding.nl_arith_repr wrapped

# 1. FStar

OUTPUT_DIR ?= obj

FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDES))

ifeq ($(OTHERFLAGS),$(subst --admit_smt_queries true,,$(OTHERFLAGS)))
FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
else
FSTAR_HINTS ?= --use_hints --use_hint_hashes
endif

# --trivial_pre_for_unannotated_effectful_fns false
#   to not enforce trivial preconditions
#   for top-level unannotated effectful functions

# 240: admitting declaration without definition
# 241: corrupt cache file AND stale cache file (argh!) we wish to make the
#      former fatal, and the latter non-fatal if it's the file we're about to
#      verify... see https://github.com/FStarLang/FStar/issues/1652
# 247: checked file not written because some of its dependencies...
# 272: top-level bindings must be total
# 274: shadowing
# 319: effectful argument, consider let binding it
# 328: definition is recursive but not used in its body
# 331: name is being ignored
# 332: abstract keyword
# 337: special treatment of @ is deprecated + Multiple decreases clauses on definition
#
# Please keep this in sync with Hacl.fst.config.json
# so the vscode extension works seamlessly.
FSTAR_NO_FLAGS = $(FSTAR_EXE) $(FSTAR_HINTS) \
  --odir $(OUTPUT_DIR) --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
  --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' \
  --warn_error '@240+241@247-272-274@319@328@331@332@337' \
  --cache_dir $(OUTPUT_DIR) --trivial_pre_for_unannotated_effectful_fns false \
  --ext context_pruning

FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS)

%.fst-in %.fsti-in:
	@echo $(FSTAR_INCLUDES)

# 2. KaRaMeL

KRML := $(KRML_HOME)/krml
$(call mustexist, KRML)

BASE_FLAGS = \
  -no-prefix 'Hacl.Frodo.Random' \
  -bundle Hacl.Spec.*,Spec.*[rename=Hacl_Spec] \
  -bundle Lib.*[rename=Hacl_Lib] \
  -drop Lib.IntVector.Intrinsics \
  -drop Lib.IntTypes.Intrinsics \
  -drop Lib.IntTypes.Intrinsics_128 \
  -fparentheses -fno-shadow -fcurly-braces -fnoreturn-else \
  -bundle Prims,C.Failure,C,C.String,C.Loops,Spec.Loops,C.Endianness,FStar.*,LowStar.*[rename=Hacl_Krmllib] \
  -bundle 'Meta.*' \
  -minimal \
  -add-early-include '<string.h>' \
  -add-early-include '"krml/internal/types.h"' \
  -add-early-include '"krml/lowstar_endianness.h"' \
  -header $(HACL_HOME)/dist/LICENSE.txt \
  -funroll-loops 16 \
  -record-renamings

CURVE_BUNDLE_SLOW= \
  -bundle Hacl.Curve25519_64_Slow
CURVE_BUNDLE_BASE= \
  $(CURVE_BUNDLE_SLOW) \
  -bundle Hacl.Impl.Curve25519.Field51[rename=Hacl_Bignum25519_51] -static-header Hacl.Impl.Curve25519.Field51 \
  -bundle Hacl.Curve25519_51=Hacl.Impl.Curve25519.Field51 \
  -bundle 'Hacl.Impl.Curve25519.\*[rename=Hacl_Curve_Leftovers]'
CURVE_BUNDLE_LOCAL=-bundle Hacl.Curve25519_64_Local=Hacl.Impl.Curve25519.Field64.Local[rename=Hacl_Curve25519_64] \
  $(CURVE_BUNDLE_BASE)
CURVE_BUNDLE=-bundle Hacl.Curve25519_64=Hacl.Impl.Curve25519.Field64.Vale \
  $(CURVE_BUNDLE_BASE) -bundle Hacl.Curve25519_64_Local

# First, match the Blake2 stuff
BLAKE2_BUNDLE_BASE= \
  -bundle Hacl.Impl.Blake2.Constants -static-header Hacl.Impl.Blake2.Constants \
  -bundle 'Hacl.Streaming.Blake2b_32=Hacl.Blake2b_32,Hacl.Hash.Blake2b_32,Hacl.Impl.Blake2.\*,Hacl.Hash.Core.Blake2,Hacl.Streaming.Blake2.Params,Hacl.Streaming.Blake2.Common[rename=Hacl_Hash_Blake2b,rename-prefix]' \
  -bundle 'Hacl.Streaming.Blake2s_32=Hacl.Blake2s_32,Hacl.Hash.Blake2s_32[rename=Hacl_Hash_Blake2s,rename-prefix]'
BLAKE2_BUNDLE= $(BLAKE2_BUNDLE_BASE) \
  -bundle Hacl.Streaming.Blake2b_256=Hacl.Blake2b_256,Hacl.Hash.Blake2b_256[rename=Hacl_Hash_Blake2b_Simd256,rename-prefix] \
  -bundle Hacl.Streaming.Blake2s_128=Hacl.Blake2s_128,Hacl.Hash.Blake2s_128[rename=Hacl_Hash_Blake2s_Simd128,rename-prefix]

# NOTE: code/hash re-exports internal Blake2 operations with the hash signature,
# but really, these should be thin wrappers that defer to the actual
# repeati-based implementation in code/blake2, as opposed to re-generating a
# copy of the code for the sole purpose of HMAC.
# TODO: make Hacl.Hash.Blake2* just inline_for_extraction wrappers that call the
# underlying implementation in code/blake2
HMAC_BUNDLE=-bundle Hacl.HMAC= \
  -bundle Hacl.HMAC.Blake2s_128= \
  -bundle Hacl.HMAC.Blake2b_256=

# Note: Hacl_Hash_SHA2 is legacy SHA2 here, will eventually go away, there's a proper
# bundle in STREAMING_BUNDLE, below
HASH_BUNDLE= \
  -bundle Hacl.Streaming.Blake2.Types+Hacl.Streaming.Types=Hacl.Streaming.MD,Spec.Hash.Definitions[rename=Hacl_Streaming_Types] \
  -bundle Hacl.Streaming.MD5=Hacl.Hash.MD5,Hacl.Hash.Core.MD5[rename=Hacl_Hash_MD5,rename-prefix] \
  -bundle Hacl.Streaming.SHA1=Hacl.Hash.SHA1,Hacl.Hash.Core.SHA1[rename=Hacl_Hash_SHA1,rename-prefix] \
  -bundle Hacl.Impl.SHA2.Types=[rename=Hacl_SHA2_Types] \
  -static-header Hacl.Impl.SHA2.Generic \
  -bundle Hacl.Streaming.SHA2=Hacl.Hash.SHA2,Hacl.Hash.Core.SHA2,Hacl.Impl.SHA2.*,Hacl.SHA2.Scalar32[rename=Hacl_Hash_SHA2,rename-prefix] \
  -bundle Hacl.Hash.Definitions=Hacl.Hash.*[rename=Hacl_Hash_Base]
# TODO: for some reason, the CSHAKE and SHA3 tests use the internal API and
# therefore Hacl.Impl.SHA3 cannot be put on the right-hand side of the bundle
# (which would eliminate internal helpers not used otherwise, such as absorb or
# squeeze)
SHA3_BUNDLE=-bundle Hacl.Streaming.Keccak+Hacl.Hash.SHA3.Scalar=Hacl.Hash.SHA3,Hacl.Impl.SHA3.Vec[rename=Hacl_Hash_SHA3,rename-prefix]
SHA3_SIMD256_BUNDLE=-bundle Hacl.Hash.SHA3.Simd256=Hacl.Impl.SHA3.Vec
CHACHA20_BUNDLE=-bundle Hacl.Chacha20=Hacl.Impl.Chacha20,Hacl.Impl.Chacha20.*
SALSA20_BUNDLE=-bundle Hacl.Salsa20=Hacl.Impl.Salsa20,Hacl.Impl.Salsa20.*,Hacl.Impl.HSalsa20
CHACHAPOLY_BUNDLE=-bundle Hacl.Impl.Chacha20Poly1305 \
  -bundle Hacl.Chacha20Poly1305_32=[rename=Hacl_AEAD_Chacha20Poly1305,rename-prefix] \
  -bundle Hacl.Chacha20Poly1305_128=[rename=Hacl_AEAD_Chacha20Poly1305_Simd128,rename-prefix] \
  -bundle Hacl.Chacha20Poly1305_256=[rename=Hacl_AEAD_Chacha20Poly1305_Simd256,rename-prefix]
ED_BUNDLE= \
  -bundle Hacl.Ed25519.PrecompTable -static-header Hacl.Ed25519.PrecompTable \
  -bundle 'Hacl.Ed25519=Hacl.Impl.Ed25519.*,Hacl.Impl.BignumQ.Mul,Hacl.Impl.Load56,Hacl.Impl.SHA512.ModQ,Hacl.Impl.Store56,Hacl.Bignum25519'
POLY_BUNDLE=-bundle 'Hacl.Streaming.Poly1305_32=Hacl.Poly1305_32,Hacl.Impl.Poly1305.Field32xN_32[rename=Hacl_MAC_Poly1305,rename-prefix]' \
  -bundle 'Hacl.Streaming.Poly1305_128=Hacl.Poly1305_128,Hacl.Impl.Poly1305.Field32xN_128[rename=Hacl_MAC_Poly1305_Simd128,rename-prefix]' \
  -bundle 'Hacl.Streaming.Poly1305_256=Hacl.Poly1305_256,Hacl.Impl.Poly1305.Field32xN_256[rename=Hacl_MAC_Poly1305_Simd256,rename-prefix]'
NACLBOX_BUNDLE=-bundle Hacl.NaCl=Hacl.Impl.SecretBox,Hacl.Impl.Box
P256_BUNDLE= \
  -bundle Hacl.P256.PrecompTable -static-header Hacl.P256.PrecompTable \
  -bundle Hacl.P256=Hacl.Impl.P256.*,Hacl.Spec.P256.*[rename=Hacl_P256]
K256_BUNDLE= \
  -bundle Hacl.K256.Field,Hacl.Impl.K256.Finv[rename=Hacl_Bignum_K256] -static-header Hacl.K256.Field,Hacl.Impl.K256.Finv \
  -bundle Hacl.K256.PrecompTable -static-header Hacl.K256.PrecompTable \
  -bundle Hacl.K256.ECDSA=Hacl.Impl.K256.*,Hacl.K256.*
FRODO_BUNDLE=-bundle 'Hacl.Frodo.KEM=Hacl.Impl.Frodo.*,Hacl.Impl.Matrix,Hacl.Frodo.*,Hacl.Keccak' -static-header Hacl.Frodo.KEM,Hacl.Impl.Frodo.*,Hacl.Impl.Matrix,Hacl.Keccak
# The only functions not marked as noextract should be in each of the Hacl.HPKE.{variants}
# Each of these module should be extracted to a different file. Therefore, this variable
# should remain empty, and overriden only when we do not want extraction of variants
HPKE_BUNDLE=-bundle Hacl.HPKE.Interface.*,Hacl.Impl.HPKE,Hacl.Meta.HPKE
STREAMING_BUNDLE=-bundle Hacl.Streaming.Interface,Hacl.Streaming.Lemmas \
  -bundle Hacl.Streaming.HMAC=Hacl.Streaming.HMAC.*,Hacl.Agile.Hash
INTTYPES_BUNDLE=-bundle Hacl.IntTypes.Intrinsics= -static-header Hacl.IntTypes.Intrinsics
INTTYPES_128_BUNDLE=-bundle Hacl.IntTypes.Intrinsics_128= -static-header Hacl.IntTypes.Intrinsics_128
RSAPSS_BUNDLE=-bundle Hacl.RSAPSS=Hacl.Impl.RSAPSS.*,Hacl.Impl.RSAPSS[rename=Hacl_RSAPSS]
FFDHE_BUNDLE=-bundle Hacl.Impl.FFDHE.Constants -static-header Hacl.Impl.FFDHE.Constants -bundle Hacl.FFDHE=Hacl.Impl.FFDHE[rename=Hacl_FFDHE]
BIGNUM_BUNDLE= \
  -bundle Hacl.Bignum.Base,Hacl.Bignum.Addition,Hacl.Bignum.Convert,Hacl.Bignum.Lib,Hacl.Bignum.Multiplication[rename=Hacl_Bignum_Base] \
  -static-header Hacl.Bignum.Base,Hacl.Bignum.Addition,Hacl.Bignum.Convert,Hacl.Bignum.Lib,Hacl.Bignum.Multiplication \
  -bundle Hacl.Bignum,Hacl.Bignum.*[rename=Hacl_Bignum]

# 3. OCaml

TAC = $(shell which tac >/dev/null 2>&1 && echo "tac" || echo "tail -r")

ALL_CMX_FILES = $(subst obj/Lib_Buffer.cmx,obj/Lib_Memzero0.cmx obj/Lib_Buffer.cmx,$(patsubst %.ml,%.cmx,$(shell echo $(ALL_ML_FILES) | $(TAC))))

# Warning 8: this pattern-matching is not exhaustive.
# Warning 20: this argument will not be used by the function.
# Warning 26: unused variable
OCAMLOPT    = eval "$(FSTAR_OCAMLENV)" && ocamlfind opt -package fstar.lib -linkpkg -thread -g -I $(HACL_HOME)/obj -w -8-20-26
OCAMLSHARED = eval "$(FSTAR_OCAMLENV)" && ocamlfind opt -shared -package fstar.pluginlib -thread -g -I $(HACL_HOME)/obj -w -8-20-26