Makefile: add FSTAR_INCLUDE_DIRS_EXTRA

fstar-helpers/Makefile.template

@@ -101,7 +101,7 @@ endef
 export FINDLIBS
 
 FINDLIBS_OUTPUT := $(shell bash -c '${FINDLIBS}')
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(FINDLIBS_OUTPUT)
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(FSTAR_INCLUDE_DIRS_EXTRA) $(FINDLIBS_OUTPUT)
 
 # Make sure FSTAR_INCLUDE_DIRS has the `proof-libs`, print hints and
 # an error message otherwise

libcrux-ml-kem/proofs/fstar/extraction/Makefile

@@ -1 +1,31 @@
+LAX_MODULES = Libcrux_ml_kem.Ind_cca.fst \
+              Libcrux_ml_kem.Ind_cpa.fst \
+              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.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.Serialize.fst \
+              Libcrux_ml_kem.Vector.Portable.Vector_type.fst \
+              Libcrux_ml_kem.Vector.Traits.fst
+
+FSTAR_INCLUDE_DIRS_EXTRA = $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.template