build: add the NO_DY build option

Makefile

@@ -3,12 +3,15 @@ FSTAR_HOME    ?= $(dir $(shell which fstar.exe))/..
 COMPARSE_HOME ?= $(MLS_HOME)/../comparse
 DY_HOME       ?= $(MLS_HOME)/../dolev-yao-star
 
-INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proofs symbolic test treedem treekem/code treekem/proofs treemath treesync/code treesync/proofs treesync/symbolic
+NO_DY ?=
+USE_DY = $(if $(NO_DY),, 1)
+
+INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proofs test treedem treekem/code treekem/proofs treemath treesync/code treesync/proofs $(if $(USE_DY), symbolic treesync/symbolic)
 
 HACL_SNAPSHOT_DIR = $(MLS_HOME)/hacl-star-snapshot
 SOURCE_DIRS = $(addprefix $(MLS_HOME)/fstar/, $(INNER_SOURCE_DIRS))
 
-INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(DY_HOME) $(DY_HOME)/symbolic
+INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(if $(USE_DY), $(DY_HOME) $(DY_HOME)/symbolic)
 FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS))
 
 ADMIT ?=
@@ -18,7 +21,7 @@ FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 FSTAR = $(FSTAR_EXE) $(MAYBE_ADMIT)
 
 DY_EXTRACT = +CryptoLib +SecrecyLabels +ComparseGlue +LabeledCryptoAPI +CryptoEffect +GlobalRuntimeLib +LabeledRuntimeAPI +Ord +AttackerAPI
-FSTAR_EXTRACT = --extract '-* +MLS +Comparse $(DY_EXTRACT) -Comparse.Tactic'
+FSTAR_EXTRACT = --extract '-* +MLS +Comparse -Comparse.Tactic $(if $(USE_DY), $(DY_EXTRACT))'
 
 # Allowed warnings:
 # - (Warning 242) Definitions of inner let-rec ... and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types

README.md

@@ -121,3 +121,6 @@ export HACL_PACKAGES_HOME=$(cd hacl-packages; pwd)
 - `make js` will compile MLS\* to Javascript
 - `node js/test.js` will start the Javascript tests
 
+Some parts of the verification can be omitted if just the extracted code is useful:
+- `NO_DY=1 make ...` will omit all the symbolic security proofs verification (hence do not require DY\* as a dependency)
+- `ADMIT=1 make ...` will admit all SMT queries