Merge branch 'dev' into dev-constant-time

fstar-helpers/Makefile.base

@@ -1,5 +1,14 @@
 # Base Makefile for F* in libcrux.
 # This inherits from Makefile.generic, and adds the `specs` folder from HACL and the `libcrux-ml-kem/proofs/fstar/spec` folder. 
 
-FSTAR_INCLUDE_DIRS_EXTRA = $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec
+VERIFY_SLOW_MODULES ?= no
+ifeq (${VERIFY_SLOW_MODULES},no)
+	ADMIT_MODULES += ${SLOW_MODULES}
+endif
+
+EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n";
+EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.';
+EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`';
+
+FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic

fstar-helpers/Makefile.generic

@@ -196,6 +196,7 @@ echo "Variables:"
 target "NO_COLOR" "Set to anything to disable colors"
 target "ADMIT_MODULES" "List of modules where F* will assume every SMT query"
 target "FSTAR_INCLUDE_DIRS_EXTRA" "List of extra include F* dirs"
+${EXTRA_HELPMESSAGE}
 endef
 export HELPMESSAGE
 
@@ -215,7 +216,6 @@ describe:
 	@printf ' - ${ANSI_COLOR_BLUE}HINT_DIR${ANSI_COLOR_RESET} = %s\n' '${HINT_DIR}'
 	@printf ' - ${ANSI_COLOR_BLUE}ADMIT_MODULE_FLAGS${ANSI_COLOR_RESET} = %s\n' '${ADMIT_MODULE_FLAGS}'
 	@printf ' - ${ANSI_COLOR_BLUE}FSTAR_INCLUDE_DIRS_EXTRA${ANSI_COLOR_RESET} = %s\n' '${FSTAR_INCLUDE_DIRS_EXTRA}'
-	@printf ' - ${ANSI_COLOR_BLUE}OTHERFLAGS${ANSI_COLOR_RESET} = %s\n' '${OTHERFLAGS}'
 
 help: ;@bash -c "$$HELPMESSAGE"
 h: ;@bash -c "$$HELPMESSAGE"

fstar-helpers/fstar-bitvec/Makefile

@@ -1,33 +1 @@
-ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \
-	      Libcrux_ml_kem.Ind_cca.fst \
-              Libcrux_ml_kem.Ind_cpa.fst \
-              Libcrux_ml_kem.Ind_cpa.fsti \
-              Libcrux_ml_kem.Invert_ntt.fst \
-              Libcrux_ml_kem.Matrix.fst \
-              Libcrux_ml_kem.Ntt.fst \
-              Libcrux_ml_kem.Polynomial.fst \
-              Libcrux_ml_kem.Sampling.fst \
-              Libcrux_ml_kem.Serialize.fst \
-	      Libcrux_ml_kem.Vector.Rej_sample_table.fsti \
-              Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst \
-              Libcrux_ml_kem.Vector.Avx2.Compress.fst \
-              Libcrux_ml_kem.Vector.Avx2.fst \
-              Libcrux_ml_kem.Vector.Avx2.Ntt.fst \
-              Libcrux_ml_kem.Vector.Avx2.Portable.fst \
-              Libcrux_ml_kem.Vector.Avx2.Sampling.fst \
-              Libcrux_ml_kem.Vector.Avx2.Serialize.fst \
-              Libcrux_ml_kem.Vector.Neon.Arithmetic.fst \
-              Libcrux_ml_kem.Vector.Neon.Compress.fst \
-              Libcrux_ml_kem.Vector.Neon.fst \
-              Libcrux_ml_kem.Vector.Neon.Ntt.fst \
-              Libcrux_ml_kem.Vector.Neon.Serialize.fst \
-              Libcrux_ml_kem.Vector.Neon.Vector_type.fst \
-              Libcrux_ml_kem.Vector.Portable.Arithmetic.fst \
-              Libcrux_ml_kem.Vector.Portable.Compress.fst \
-              Libcrux_ml_kem.Vector.Portable.Ntt.fst \
-              Libcrux_ml_kem.Vector.Portable.Sampling.fst \
-              Libcrux_ml_kem.Vector.Portable.Vector_type.fst \
-              Libcrux_ml_kem.Vector.Traits.fst
-
-OTHERFLAGS += --unsafe_tactic_exec
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.base