Revision 200ca2955cb6a62574c9a3ddf91a7243ac348c6b authored by Jonathan Protzenko on 01 April 2020, 00:17:13 UTC, committed by GitHub on 01 April 2020, 00:17:13 UTC
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
HACL_HOME ?= .
# Put your local configuration (e.g. HACL_HOME, KREMLIN_HOME, etc.) in
# Makefile.config
-include $(HACL_HOME)/Makefile.config
KREMLIN_HOME ?= $(HACL_HOME)/../kremlin
FSTAR_HOME ?= $(HACL_HOME)/../FStar
VALE_HOME ?= $(HACL_HOME)/../vale
include $(HACL_HOME)/Makefile.include
INCLUDES = \
$(ALL_HACL_DIRS) \
$(FSTAR_HOME)/ulib/.cache \
$(KREMLIN_HOME)/kremlib
# 0. Vale
VALE_FSTAR_FLAGS=--z3cliopt smt.arith.nl=false \
--z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 \
--use_extracted_interfaces true \
--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
# 272: top-level bindings must be total
# 247: checked file not written because some of its dependencies...
# 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
FSTAR_NO_FLAGS = $(FSTAR_HOME)/bin/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 '+241@247-272' \
--cache_dir $(OUTPUT_DIR) --trivial_pre_for_unannotated_effectful_fns false
FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS)
%.fst-in %.fsti-in:
@echo $(FSTAR_INCLUDES)
# 2. Kremlin
KRML = $(KREMLIN_HOME)/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 \
-fparentheses -fno-shadow -fcurly-braces -fnoreturn-else \
-bundle Prims,C.Failure,C,C.String,C.Loops,Spec.Loops,C.Endianness,FStar.*,LowStar.*[rename=Hacl_Kremlib] \
-bundle 'Meta.*' \
-minimal \
-add-include '"kremlin/internal/types.h"' \
-add-include '"kremlin/lowstar_endianness.h"' \
-add-include '<string.h>' \
-header $(HACL_HOME)/dist/LICENSE.txt
CURVE_BUNDLE_SLOW= \
-bundle 'Hacl.Curve25519_64_Slow=Hacl.Impl.Curve25519.Field64.Hacl,Hacl.Spec.Curve25519,Hacl.Spec.Curve25519.\*'
CURVE_BUNDLE_BASE= \
$(CURVE_BUNDLE_SLOW) \
-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
HASH_BUNDLE=-bundle Hacl.Hash.MD5+Hacl.Hash.Core.MD5+Hacl.Hash.SHA1+Hacl.Hash.Core.SHA1+Hacl.Hash.SHA2+Hacl.Hash.Core.SHA2=Hacl.Hash.*[rename=Hacl_Hash]
SHA3_BUNDLE=-bundle Hacl.Impl.SHA3+Hacl.SHA3=[rename=Hacl_SHA3]
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
BLAKE2_BUNDLE=-bundle Hacl.Impl.Blake2.Constants -static-header Hacl.Impl.Blake2.Constants -bundle 'Hacl.Impl.Blake2.\*'
ED_BUNDLE=-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.Poly1305_32=Hacl.Impl.Poly1305.Field32xN_32' \
-bundle 'Hacl.Poly1305_128=Hacl.Impl.Poly1305.Field32xN_128' \
-bundle 'Hacl.Poly1305_256=Hacl.Impl.Poly1305.Field32xN_256'
NACLBOX_BUNDLE=-bundle Hacl.NaCl=Hacl.Impl.SecretBox,Hacl.Impl.Box
ECDSA_BUNDLE=-bundle Hacl.Impl.ECDSA=Hacl.Impl.ECDSA,Hacl.Impl.ECDSA.*,Hacl.Impl.P256.*,Hacl.Hash.SHA2,Hacl.Hash.Core.SHA2,Hacl.Hash.Core.SHA2.Constants,Hacl.Hash.Definitions,Hacl.Impl.P256,Hacl.Spec.P256.*,Hacl.Impl.SolinasReduction,Hacl.Impl.LowLevel[rename=Hacl_ECDSA]
FRODO_BUNDLE=-bundle 'Hacl.Frodo.KEM=Frodo.Params,Hacl.Impl.Frodo.*,Hacl.Impl.Matrix,Hacl.Frodo.*,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.*
# 3. OCaml
TAC = $(shell which tac >/dev/null 2>&1 && echo "tac" || echo "tail -r")
ALL_CMX_FILES = $(patsubst %.ml,%.cmx,$(shell echo $(ALL_ML_FILES) | $(TAC)))
ifeq ($(OS),Windows_NT)
export OCAMLPATH := $(FSTAR_HOME)/bin;$(OCAMLPATH)
else
export OCAMLPATH := $(FSTAR_HOME)/bin:$(OCAMLPATH)
endif
# Warning 8: this pattern-matching is not exhaustive.
# Warning 20: this argument will not be used by the function.
# Warning 26: unused variable
OCAMLOPT = ocamlfind opt -package fstarlib -linkpkg -g -I $(HACL_HOME)/obj -w -8-20-26
OCAMLSHARED = ocamlfind opt -shared -package fstar-tactics-lib -g -I $(HACL_HOME)/obj -w -8-20-26
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...