From 6beb51b60b80b8e96258001d8089c7471ad54b31 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 6 May 2024 11:59:19 +0200 Subject: [PATCH] feat: Makefiles: find include dirs via `cargo metadata` --- .../barrett/proofs/fstar/extraction/Makefile | 102 +++++++++++----- .../chacha20/proofs/fstar/extraction/Makefile | 110 +++++++++++++----- examples/default.nix | 13 ++- .../proofs/fstar/extraction/Makefile | 103 +++++++++++----- examples/limited-order-book/Cargo.toml | 1 + .../proofs/fstar/extraction/Makefile | 101 +++++++++++----- .../sha256/proofs/fstar/extraction/Makefile | 103 +++++++++++----- hax-lib/proofs/fstar/extraction/Makefile | 102 +++++++++++----- 8 files changed, 463 insertions(+), 172 deletions(-) diff --git a/examples/barrett/proofs/fstar/extraction/Makefile b/examples/barrett/proofs/fstar/extraction/Makefile index f976e19da..df5df7a06 100644 --- a/examples/barrett/proofs/fstar/extraction/Makefile +++ b/examples/barrett/proofs/fstar/extraction/Makefile @@ -4,16 +4,21 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# 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_PROOF_LIBS to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`. +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # -# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -30,17 +35,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_HOME ?= $(shell git rev-parse --show-toplevel) -FSTAR_HOME ?= $(HAX_HOME)/../../../FStar -HACL_HOME ?= $(HAX_HOME)/../../../hacl-star +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +CACHE_DIR ?= .cache +HINT_DIR ?= .hints -HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction +SHELL ?= /usr/bin/env bash -CACHE_DIR ?= $(HAX_PROOF_LIBS)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS)/.hints +EXECUTABLES = cargo cargo-hax jq +K := $(foreach bin,$(EXECUTABLES),\ + $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) .PHONY: all verify clean @@ -48,17 +53,63 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# By default, we process all the files in the current directory. Here, we -# *extend* the set of relevant files with the tests. -ROOTS = Barrett.fst - -$(ROOTS): ../../../src/lib.rs - cargo hax into fstar --z3rlimit 500 - -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) +# Default hax invocation +HAX_CLI = "cargo hax into fstar" + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# If no any F* file is detected, we run hax +ifeq "$(wildcard *.fst *fsti)" "" +$(shell $(SHELL) -c $(HAX_CLI)) +endif + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# Regenerate F* files via hax when Rust sources change +$(ROOTS): $(shell find ../../../src -type f -name '*.rs') + $(shell $(SHELL) -c $(HAX_CLI)) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -68,7 +119,6 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) - .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -99,8 +149,6 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets -SHELL ?= /usr/bin/env bash - clean: rm -rf $(CACHE_DIR)/* rm *.fst diff --git a/examples/chacha20/proofs/fstar/extraction/Makefile b/examples/chacha20/proofs/fstar/extraction/Makefile index 6521ef5ac..381ef237b 100644 --- a/examples/chacha20/proofs/fstar/extraction/Makefile +++ b/examples/chacha20/proofs/fstar/extraction/Makefile @@ -4,16 +4,21 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# 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_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # -# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -30,17 +35,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_HOME ?= $(shell git rev-parse --show-toplevel) -FSTAR_HOME ?= $(HAX_HOME)/../../../FStar -HACL_HOME ?= $(HAX_HOME)/../../../hacl-star +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +CACHE_DIR ?= .cache +HINT_DIR ?= .hints -HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction +SHELL ?= /usr/bin/env bash -CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints +EXECUTABLES = cargo cargo-hax jq +K := $(foreach bin,$(EXECUTABLES),\ + $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) .PHONY: all verify clean @@ -48,18 +53,63 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# By default, we process all the files in the current directory. Here, we -# *extend* the set of relevant files with the tests. -ROOTS = Chacha20.fst Chacha20.Hacspec_helper.fst - -$(ROOTS): ../../../src/lib.rs ../../../src/hacspec_helper.rs - cargo hax into fstar - -FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ - $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ - $(HAX_LIBS_HOME)/proofs/fstar/extraction \ - $(HAX_LIBS_HOME)/../../hax-bounded-integers/proofs/fstar/extraction \ - $(HAX_LIBS_HOME) +# Default hax invocation +HAX_CLI = "cargo hax into fstar" + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# If no any F* file is detected, we run hax +ifeq "$(wildcard *.fst *fsti)" "" +$(shell $(SHELL) -c $(HAX_CLI)) +endif + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# Regenerate F* files via hax when Rust sources change +$(ROOTS): $(shell find ../../../src -type f -name '*.rs') + $(shell $(SHELL) -c $(HAX_CLI)) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -69,7 +119,6 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) - .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -82,9 +131,6 @@ $(HINT_DIR): $(CACHE_DIR): mkdir -p $@ -$(CACHE_DIR)/Chacha20.Hacspec_helper.fst.checked: | .depend $(HINT_DIR) $(CACHE_DIR) - $(FSTAR) --lax $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints - $(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) $(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints @@ -103,8 +149,10 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets -SHELL ?= /usr/bin/env bash - clean: rm -rf $(CACHE_DIR)/* rm *.fst + +# Special rule for `Chacha20.Hacspec_helper` +$(CACHE_DIR)/Chacha20.Hacspec_helper.fst.checked: | .depend $(HINT_DIR) $(CACHE_DIR) + $(FSTAR) --lax $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints diff --git a/examples/default.nix b/examples/default.nix index 42759e00e..74aba3dcd 100644 --- a/examples/default.nix +++ b/examples/default.nix @@ -6,16 +6,19 @@ fstar, hacl-star, hax-env, + jq, }: let + matches = re: path: !builtins.isNull (builtins.match re path); commonArgs = { version = "0.0.1"; src = lib.cleanSourceWith { src = craneLib.path ./..; filter = path: type: - # We include only certain files, notably we exclude generated - # files (`.fst`, `.v`, etc.) - !builtins.isNull (builtins.match ".*(Makefile|.*[.](rs|toml|lock|diff))$" path) - || ("directory" == type); + # We include only certain files. FStar files under the example + # directory are listed out. + ( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?))$" path + && !matches ".*examples/.*[.]fsti?$" path + ) || ("directory" == type); }; doCheck = false; cargoVendorDir = craneLib.vendorMultipleCargoDeps { @@ -43,5 +46,5 @@ in sed -i "s/make -C limited-order-book/HAX_VANILLA_RUSTC=never make -C limited-order-book/g" Makefile make ''; - buildInputs = [hax hax-env fstar]; + buildInputs = [hax hax-env fstar jq]; }) diff --git a/examples/kyber_compress/proofs/fstar/extraction/Makefile b/examples/kyber_compress/proofs/fstar/extraction/Makefile index 2cfa01554..df5df7a06 100644 --- a/examples/kyber_compress/proofs/fstar/extraction/Makefile +++ b/examples/kyber_compress/proofs/fstar/extraction/Makefile @@ -4,16 +4,21 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# 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_PROOF_LIBS to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`. +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # -# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -30,18 +35,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_HOME ?= $(shell git rev-parse --show-toplevel) -FSTAR_HOME ?= $(HAX_HOME)/../../../FStar -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") +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +CACHE_DIR ?= .cache +HINT_DIR ?= .hints -HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction +SHELL ?= /usr/bin/env bash -CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints +EXECUTABLES = cargo cargo-hax jq +K := $(foreach bin,$(EXECUTABLES),\ + $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) .PHONY: all verify clean @@ -49,17 +53,63 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# By default, we process all the files in the current directory. Here, we -# *extend* the set of relevant files with the tests. -ROOTS = Kyber_compress.fst - -$(ROOTS): ../../../src/lib.rs - cargo hax into fstar --z3rlimit 200 - -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) +# Default hax invocation +HAX_CLI = "cargo hax into fstar" + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# If no any F* file is detected, we run hax +ifeq "$(wildcard *.fst *fsti)" "" +$(shell $(SHELL) -c $(HAX_CLI)) +endif + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# Regenerate F* files via hax when Rust sources change +$(ROOTS): $(shell find ../../../src -type f -name '*.rs') + $(shell $(SHELL) -c $(HAX_CLI)) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -69,7 +119,6 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) - .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -100,8 +149,6 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets -SHELL ?= /usr/bin/env bash - clean: rm -rf $(CACHE_DIR)/* rm *.fst diff --git a/examples/limited-order-book/Cargo.toml b/examples/limited-order-book/Cargo.toml index 9f437b1ec..a7410d98e 100644 --- a/examples/limited-order-book/Cargo.toml +++ b/examples/limited-order-book/Cargo.toml @@ -12,4 +12,5 @@ crate-type = ["cdylib", "lib"] candid = "0.9.6" ic-cdk = "0.10.0" ic-cdk-macros = "0.8.1" +hax-lib.workspace = true serde = { version = "1.0" } diff --git a/examples/limited-order-book/proofs/fstar/extraction/Makefile b/examples/limited-order-book/proofs/fstar/extraction/Makefile index e83a9affc..0183a6dd6 100644 --- a/examples/limited-order-book/proofs/fstar/extraction/Makefile +++ b/examples/limited-order-book/proofs/fstar/extraction/Makefile @@ -4,16 +4,21 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# 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_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # -# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -30,17 +35,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_HOME ?= $(shell git rev-parse --show-toplevel) -FSTAR_HOME ?= $(HAX_HOME)/../../../FStar -HACL_HOME ?= $(HAX_HOME)/../../../hacl-star +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +CACHE_DIR ?= .cache +HINT_DIR ?= .hints -HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction +SHELL ?= /usr/bin/env bash -CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints +EXECUTABLES = cargo cargo-hax jq +K := $(foreach bin,$(EXECUTABLES),\ + $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) .PHONY: all verify clean @@ -48,17 +53,62 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# By default, we process all the files in the current directory. Here, we -# *extend* the set of relevant files with the tests. -ROOTS = Lob_backend.fst - -$(ROOTS): ../../../src/canister.rs ../../../src/lib.rs - cargo hax into -i '-** +**::process_order' fstar - -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) +HAX_CLI = "cargo hax into -i '-** +**::process_order' fstar" + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# If no any F* file is detected, we run hax +ifeq "$(wildcard *.fst *fsti)" "" +$(shell $(SHELL) -c $(HAX_CLI)) +endif + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# Regenerate F* files via hax when Rust sources change +$(ROOTS): $(shell find ../../../src -type f -name '*.rs') + $(shell $(SHELL) -c $(HAX_CLI)) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -68,7 +118,6 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) - .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -99,8 +148,6 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets -SHELL ?= /usr/bin/env bash - clean: rm -rf $(CACHE_DIR)/* rm *.fst diff --git a/examples/sha256/proofs/fstar/extraction/Makefile b/examples/sha256/proofs/fstar/extraction/Makefile index f51e75f8e..df5df7a06 100644 --- a/examples/sha256/proofs/fstar/extraction/Makefile +++ b/examples/sha256/proofs/fstar/extraction/Makefile @@ -4,16 +4,21 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# 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_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # -# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -30,17 +35,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_HOME ?= $(shell git rev-parse --show-toplevel) -FSTAR_HOME ?= $(HAX_HOME)/../../../FStar -HACL_HOME ?= $(HAX_HOME)/../../../hacl-star +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +CACHE_DIR ?= .cache +HINT_DIR ?= .hints -HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction +SHELL ?= /usr/bin/env bash -CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints +EXECUTABLES = cargo cargo-hax jq +K := $(foreach bin,$(EXECUTABLES),\ + $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) .PHONY: all verify clean @@ -48,17 +53,63 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# By default, we process all the files in the current directory. Here, we -# *extend* the set of relevant files with the tests. -ROOTS = Sha256.fst - -$(ROOTS): - cargo hax into fstar - -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) +# Default hax invocation +HAX_CLI = "cargo hax into fstar" + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# If no any F* file is detected, we run hax +ifeq "$(wildcard *.fst *fsti)" "" +$(shell $(SHELL) -c $(HAX_CLI)) +endif + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# Regenerate F* files via hax when Rust sources change +$(ROOTS): $(shell find ../../../src -type f -name '*.rs') + $(shell $(SHELL) -c $(HAX_CLI)) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -68,7 +119,6 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) - .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -99,7 +149,6 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets -SHELL ?= /usr/bin/env bash - clean: rm -rf $(CACHE_DIR)/* + rm *.fst diff --git a/hax-lib/proofs/fstar/extraction/Makefile b/hax-lib/proofs/fstar/extraction/Makefile index b6518ff90..df5df7a06 100644 --- a/hax-lib/proofs/fstar/extraction/Makefile +++ b/hax-lib/proofs/fstar/extraction/Makefile @@ -4,16 +4,21 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# 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_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. -# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # -# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -30,17 +35,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_HOME ?= $(shell git rev-parse --show-toplevel) -FSTAR_HOME ?= $(HAX_HOME)/../../../FStar -HACL_HOME ?= $(HAX_HOME)/../../../hacl-star +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +CACHE_DIR ?= .cache +HINT_DIR ?= .hints -HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar -HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction +SHELL ?= /usr/bin/env bash -CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints +EXECUTABLES = cargo cargo-hax jq +K := $(foreach bin,$(EXECUTABLES),\ + $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) .PHONY: all verify clean @@ -48,14 +53,63 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# By default, we process all the files in the current directory. Here, we -# *extend* the set of relevant files with the tests. -ROOTS = $(*.fst) - -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) +# Default hax invocation +HAX_CLI = "cargo hax into fstar" + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# If no any F* file is detected, we run hax +ifeq "$(wildcard *.fst *fsti)" "" +$(shell $(SHELL) -c $(HAX_CLI)) +endif + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# Regenerate F* files via hax when Rust sources change +$(ROOTS): $(shell find ../../../src -type f -name '*.rs') + $(shell $(SHELL) -c $(HAX_CLI)) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -65,7 +119,6 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) - .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -78,9 +131,6 @@ $(HINT_DIR): $(CACHE_DIR): mkdir -p $@ -$(CACHE_DIR)/Chacha20.Hacspec_helper.fst.checked: | .depend $(HINT_DIR) $(CACHE_DIR) - $(FSTAR) --lax $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints - $(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) $(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints @@ -99,8 +149,6 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets -SHELL ?= /usr/bin/env bash - clean: rm -rf $(CACHE_DIR)/* rm *.fst