-
Notifications
You must be signed in to change notification settings - Fork 161
/
Makefile.common
246 lines (208 loc) · 11.2 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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
# 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
ifndef KRML_HOME
# assuming an Everest source tree
KRML_HOME := $(HACL_HOME)/../karamel
endif
ifndef FSTAR_HOME
FSTAR_EXE=$(shell which fstar.exe)
ifeq ($(FSTAR_EXE),)
# F* not found in PATH, assuming an Everest source tree
FSTAR_HOME := $(HACL_HOME)/../FStar
else
# F* found in PATH, assuming directory name ends with /bin
FSTAR_HOME := $(dir $(FSTAR_EXE))/..
endif
endif
FSTAR_EXE := $(FSTAR_HOME)/bin/fstar.exe
ifndef FSTAR_ULIB
FSTAR_ULIB := $(shell if test -d "$(FSTAR_HOME)/ulib" ; then echo "$(FSTAR_HOME)/ulib" ; else echo "$(FSTAR_HOME)/lib/fstar" ; fi)
endif
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_HOME := $(call sanitize_path,$(FSTAR_HOME))
FSTAR_ULIB := $(call sanitize_path,$(FSTAR_ULIB))
VALE_HOME := $(call sanitize_path,$(VALE_HOME))
include $(HACL_HOME)/Makefile.include
# $(FSTAR_ULIB)/.cache necessary for Vale
INCLUDES = \
$(ALL_HACL_DIRS) \
$(FSTAR_ULIB)/.cache \
$(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
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 \
-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.MD,Spec.Hash.Definitions,Hacl.Streaming.Types[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
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)/lib;$(OCAMLPATH)
else
export OCAMLPATH := $(FSTAR_HOME)/lib:$(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_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs" ocamlfind opt -package fstar.lib -linkpkg -thread -g -I $(HACL_HOME)/obj -w -8-20-26
OCAMLSHARED = OCAMLFIND_IGNORE_DUPS_IN="`ocamlc -where`/compiler-libs" ocamlfind opt -shared -package fstar.lib -thread -g -I $(HACL_HOME)/obj -w -8-20-26