Skip to content

Commit

Permalink
feat: Makefiles: find include dirs via cargo metadata
Browse files Browse the repository at this point in the history
  • Loading branch information
@W95Psp
W95Psp committed May 6, 2024
1 parent b2602e0 commit 46b3eca
Show file tree
Hide file tree
Showing 8 changed files with 461 additions and 172 deletions.
101 changes: 74 additions & 27 deletions examples/barrett/proofs/fstar/extraction/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
#
Expand All @@ -30,35 +35,80 @@
# (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

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)
HAX_CLI = "cargo hax into fstar --z3rlimit 500"

# 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 \
Expand All @@ -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' > $@
Expand Down Expand Up @@ -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
110 changes: 79 additions & 31 deletions examples/chacha20/proofs/fstar/extraction/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
#
Expand All @@ -30,36 +35,81 @@
# (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

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 \
Expand All @@ -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' > $@
Expand All @@ -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

Expand All @@ -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
13 changes: 8 additions & 5 deletions examples/default.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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];
})
Loading

0 comments on commit 46b3eca

Please sign in to comment.