fix: misc fixes to Makefiles and Nix

The Makefiles are all over the place (in hax proof libs, hax examples, Bertie, Libcrux), and they don't rely on exactly the same env vars. This commit fixes a few of those differences. This commit also helps for PR cryspen/libcrux#210.
hacspec · Mar 6, 2024 · 902f784 · 902f784
1 parent ee963ae
commit 902f784
Show file tree

Hide file tree

Showing 6 changed files with 32 additions and 18 deletions.
diff --git a/examples/chacha20/proofs/fstar/extraction/Makefile b/examples/chacha20/proofs/fstar/extraction/Makefile
@@ -37,7 +37,7 @@ HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
 FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
 HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
-HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib
+HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
 
 CACHE_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.cache
 HINT_DIR       ?= $(HAX_PROOF_LIBS_HOME)/.hints
@@ -58,7 +58,7 @@ $(ROOTS): ../../../src/lib.rs ../../../src/hacspec_helper.rs
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
 	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
 	$(HAX_PROOF_LIBS_HOME)/hax_lib \
-	$(HAX_LIBS_HOME)/proofs/fstar/extraction
+	$(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/examples/limited-order-book/proofs/fstar/extraction/Makefile b/examples/limited-order-book/proofs/fstar/extraction/Makefile
@@ -37,7 +37,7 @@ HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
 FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
 HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
-HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib
+HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
 
 CACHE_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.cache
 HINT_DIR       ?= $(HAX_PROOF_LIBS_HOME)/.hints
@@ -58,7 +58,7 @@ $(ROOTS): ../../../src/canister.rs ../../../src/lib.rs
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
 	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
 	$(HAX_PROOF_LIBS_HOME)/hax_lib \
-	$(HAX_LIBS_HOME)/proofs/fstar/extraction
+	$(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/examples/sha256/proofs/fstar/extraction/Makefile b/examples/sha256/proofs/fstar/extraction/Makefile
@@ -37,7 +37,7 @@ HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
 FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
 HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
-HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib
+HAX_LIBS_HOME        ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
 
 CACHE_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.cache
 HINT_DIR       ?= $(HAX_PROOF_LIBS_HOME)/.hints
@@ -58,7 +58,7 @@ $(ROOTS):
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
 	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
 	$(HAX_PROOF_LIBS_HOME)/hax_lib \
-	$(HAX_LIBS_HOME)/proofs/fstar/extraction
+	$(HAX_LIBS_HOME)
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/flake.nix b/flake.nix
@@ -43,7 +43,7 @@
         fstar = inputs.fstar.packages.${system}.default;
         hax-env-file = pkgs.writeText "hax-env-file" ''
           HAX_PROOF_LIBS_HOME="${./proof-libs/fstar}"
-          HAX_LIBS_HOME="${./hax-lib}"
+          HAX_LIBS_HOME="${./hax-lib}"/proofs/fstar/extraction
           HACL_HOME="${hacl-star}"
         '';
         hax-env = pkgs.writeScriptBin "hax-env" ''
@@ -151,8 +151,13 @@
         in {
           fstar = pkgs.mkShell {
             inherit inputsFrom LIBCLANG_PATH;
-            shellHook = "eval $(hax-env)";
-            packages = packages ++ [fstar hax-env];
+            HACL_HOME = "${hacl-star}";
+            shellHook = ''
+              HAX_ROOT=$(git rev-parse --show-toplevel)
+              export HAX_PROOF_LIBS_HOME="$HAX_ROOT/proof-libs/fstar"
+              export HAX_LIBS_HOME="$HAX_ROOT/hax-lib"
+            '';
+            packages = packages ++ [fstar];
           };
           default = pkgs.mkShell {
             inherit packages inputsFrom LIBCLANG_PATH;

diff --git a/proof-libs/fstar/core/Makefile b/proof-libs/fstar/core/Makefile
@@ -29,13 +29,17 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_PROOF_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
-FSTAR_HOME    ?= $(HAX_PROOF_LIBS_HOME)/../../../FStar
-HACL_HOME     ?= $(HAX_PROOF_LIBS_HOME)/../../../hacl-star
+
+HAX_HOME      ?= $(shell git rev-parse --show-toplevel)
+FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
+HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
-CACHE_DIR     ?= $(HAX_PROOF_LIBS_HOME)/.cache
-HINT_DIR      ?= $(HAX_PROOF_LIBS_HOME)/.hints
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib
+
+CACHE_DIR     ?= ../core/.cache
+HINT_DIR      ?= ../core/.hints
 
 .PHONY: all verify clean
 
@@ -47,7 +51,8 @@ all:
 # *extend* the set of relevant files with the tests.
 ROOTS = $(wildcard *.fst)
 
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_PROOF_LIBS_HOME)/hax_lib
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)/proofs/fstar/extraction/
+
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \

diff --git a/proof-libs/fstar/rust_primitives/Makefile b/proof-libs/fstar/rust_primitives/Makefile
@@ -6,7 +6,8 @@
 #
 # We expect FSTAR_HOME to be set to your FSTAR repo/install directory
 # We expect HACL_HOME to be set to your HACL* repo location
-# We expect HAX_LIBS_HOME to be set to the folder containing core, rust_primitives etc.
+# We expect HAX_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc.
+# We expect HAX_LIBS_HOME to be set to the hax-lib folder
 #
 # ROOTS contains all the top-level F* files you wish to verify
 # The default target `verify` verified ROOTS and its dependencies
@@ -29,11 +30,14 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
+HAX_HOME      ?= $(shell git rev-parse --show-toplevel)
 FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
 HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
 
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib
+
 CACHE_DIR     ?= $(HAX_LIBS_HOME)/.cache
 HINT_DIR      ?= $(HAX_LIBS_HOME)/.hints
 
@@ -47,7 +51,7 @@ all:
 # *extend* the set of relevant files with the tests.
 ROOTS = $(wildcard *.fst)
 
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_LIBS_HOME)/rust_primitives $(HAX_LIBS_HOME)/core $(HAX_LIBS_HOME)/hax_lib
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)/proofs/fstar/extraction/
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \