forked from hacl-star/hacl-star
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Makefile.common
171 lines (142 loc) · 7.72 KB
/
Makefile.common
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
# 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 ?= $(shell pwd)
# Put your local configuration (e.g. HACL_HOME, KRML_HOME, etc.) in
# Makefile.config
-include $(HACL_HOME)/Makefile.config
KRML_HOME ?= $(HACL_HOME)/../karamel
FSTAR_HOME ?= $(HACL_HOME)/../FStar
VALE_HOME ?= $(HACL_HOME)/../vale
include $(HACL_HOME)/Makefile.include
INCLUDES = \
$(ALL_HACL_DIRS) \
$(FSTAR_HOME)/ulib/.cache \
$(KRML_HOME)/krmllib/obj \
$(KRML_HOME)/krmllib
# 0. Vale
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
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 '@240+241@247-272-274@319@328@331@332@337' \
--cache_dir $(OUTPUT_DIR) --trivial_pre_for_unannotated_effectful_fns false
FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS)
%.fst-in %.fsti-in:
@echo $(FSTAR_INCLUDES)
# 2. KaRaMeL
KRML = $(KRML_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 \
-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
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.Blake2b_32+Hacl.Blake2s_32=Hacl.Hash.Blake2,Hacl.Impl.Blake2.\*,Hacl.Hash.Core.Blake2[rename=Hacl_Hash_Blake2]'
BLAKE2_BUNDLE= $(BLAKE2_BUNDLE_BASE) \
-bundle Hacl.Blake2b_256=Hacl.Hash.Blake2b_256[rename=Hacl_Hash_Blake2b_256] \
-bundle Hacl.Blake2s_128=Hacl.Hash.Blake2s_128[rename=Hacl_Hash_Blake2s_128]
HASH_BUNDLE= \
-bundle Hacl.Hash.MD5=Hacl.Hash.Core.MD5 \
-bundle Hacl.Hash.SHA1=Hacl.Hash.Core.SHA1 \
-bundle Hacl.Hash.SHA2=Hacl.Hash.Core.SHA2 \
-bundle Hacl.Hash.Definitions=Hacl.Hash.*[rename=Hacl_Hash_Base]
SHA2MB_BUNDLE= -bundle Hacl.Impl.SHA2.Types=[rename=Hacl_SHA2_Types] \
-bundle Hacl.Impl.SHA2.Generic,Hacl.Impl.SHA2.*[rename=Hacl_SHA2_Generic] -static-header Hacl.Impl.SHA2.Generic
SHA3_BUNDLE=-bundle Hacl.Impl.SHA3+Hacl.SHA3=Hacl.Hash.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
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.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
P256_BUNDLE=-bundle Hacl.P256=Hacl.Impl.ECDSA.*,Hacl.Impl.SolinasReduction,Hacl.Impl.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.SHA2=Hacl.SHA2.Scalar32
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))))
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