Template makefile for hax and F* verification

Makefile

# 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`, `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
#
# (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

EXECUTABLES = cargo cargo-hax jq
K := $(foreach exec,$(EXECUTABLES),\
        $(if $(shell which $(exec)),some string,$(error "No $(exec) in PATH")))

.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}"

# If no any F* file is detected, we run hax
ifeq "$(wildcard *.fst *fsti)" ""
$(shell cargo hax into fstar)
endif

# 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 = \
  --warn_error '-331 -321 -274' \
  --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) $(HACL_HOME)
	$(info $(ROOTS))
	$(FSTAR) --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@

include .depend

$(HINT_DIR):
	mkdir -p $@

$(CACHE_DIR):
	mkdir -p $@

$(CACHE_DIR)/%.checked: | enforce_proof_libs .depend $(HINT_DIR) $(CACHE_DIR) $(HACL_HOME)
	$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints

verify: enforce_proof_libs $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) $(HACL_HOME)

# 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)

hax.fst.config.json: enforce_proof_libs
	@echo "$(FSTAR_INCLUDE_DIRS)" | jq --arg fstar "$(FSTAR_BIN)" -R 'split(" ") | {fstar_exe: $$fstar, includes: .}' > $@

vscode: hax.fst.config.json

enforce_proof_libs:
	@if echo "$(FSTAR_INCLUDE_DIRS)" | grep 'proof-libs/fstar' > /dev/null; then :; else \
printf '\n\033[1m\033[31mError: could not detect `proof-libs`!\033[0m\n  > Do you have `hax-lib` in your `Cargo.toml` as a **git** dependency?\n  \033[34m> Tip: you may want to run `cargo add --git https://github.com/hacspec/hax hax-lib`\033[0m\n\n' ; \
false ; \
fi

# Clean targets

SHELL=bash

clean:
	rm -rf $(CACHE_DIR)/*
	rm *.fst