Last active
March 20, 2024 21:30
-
-
Save W95Psp/4c304132a1f85c5af4e4959dd6b356c3 to your computer and use it in GitHub Desktop.
Template makefile for hax and F* verification
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# This is a generically useful Makefile for F* that is self-contained | |
# | |
# It is tempting to factor this out into multiple Makefiles but that | |
# makes it less portable, so resist temptation, or move to a more | |
# sophisticated build system. | |
# | |
# 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`, `hax` and `rustup` 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 | |
# | |
# (setq-default fstar-executable "<YOUR_FSTAR_HOME>/bin/fstar.exe") | |
# (setq-default fstar-smt-executable "<YOUR_Z3_HOME>/bin/z3") | |
# | |
# (defun my-fstar-compute-prover-args-using-make () | |
# "Construct arguments to pass to F* by calling make." | |
# (with-demoted-errors "Error when constructing arg string: %S" | |
# (let* ((fname (file-name-nondirectory buffer-file-name)) | |
# (target (concat fname "-in")) | |
# (argstr (car (process-lines "make" "--quiet" target)))) | |
# (split-string argstr)))) | |
# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) | |
# | |
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 | |
.PHONY: all verify clean | |
all: | |
rm -f .depend && $(MAKE) .depend | |
$(MAKE) verify | |
# 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}" | |
# By default, we process all the files in the current directory | |
ROOTS = $(wildcard *.fst *fsti) | |
# 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 \ | |
--cache_checked_modules --cache_dir $(CACHE_DIR) \ | |
--already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \ | |
$(addprefix --include ,$(FSTAR_INCLUDE_DIRS)) | |
FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) | |
.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) | |
$(info $(ROOTS)) | |
$(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ | |
include .depend | |
$(HINT_DIR): | |
mkdir -p $@ | |
$(CACHE_DIR): | |
mkdir -p $@ | |
$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) | |
$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints | |
verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) | |
# Targets for interactive mode | |
%.fst-in: | |
$(info $(FSTAR_FLAGS) \ | |
$(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints) | |
%.fsti-in: | |
$(info $(FSTAR_FLAGS) \ | |
$(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints) | |
# Clean targets | |
SHELL=bash | |
clean: | |
rm -rf $(CACHE_DIR)/* | |
rm *.fst | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment