Tooling and project setup¶

For the sake of this tutorial, we use a sample project that provides a toy implementation of bignum addition in C. The project is located in the karamel repository, under the book/tutorial directory.

The sample project has a minimal specification, a corresponding implementation, a powerful build system that should cover most common situations and a set of C tests. In short, we hope that this will set a reference style for all new Low* projects.

We now describe how to get a working setup – subsequent sections will take a deeper look at the code.

Installing the tools¶

We recommend using the Everest script, if only for its z3 and opam commands, to make sure you have the exact version of the tools we need. All of our proofs are intimately tied to a specific version of F*, and if you’re not running the right one, you may have trouble even building F*’s standard library.

$ ./everest z3 opam

Then, you can either install F* and KaRaMeL yourself, or rely on the Everest script for that purpose:

$ ./everest pull FStar make karamel make

For a nix flake based install use

$ nix shell

In any case, remember to export suitable values for the FSTAR_HOME and KRML_HOME environment variables once you’re done.

We strongly recommend using the fstar-mode.el Emacs plugin for interactive mode support.

Note

There is an extra customization step which allows querying a Makefile to figure out the arguments to pass to F*; please follow instructions at https://github.com/project-everest/mitls-fstar#configuring-emacs-mode – this is used pretty pervasively throughout all of the Everest projects and the sample project uses it too.

Directory structure¶

We adopt the following canonical and recommended structure for the toy project.

code: low-level implementation in Low*, extracts to C
code/c: hand-written C code (unverified), linked with the extracted Low* code
specs: high-level specifications, extract to OCaml for specs testing
specs/ml: hand-written OCaml code (unverified), linked with the extracted OCaml specifications
obj: F* and OCaml build artifacts, i.e. whatever is covered by F*’s --depend facility: .checked files (binary serialized build products once a file has been verified), .ml files (the result of F* extracting to OCaml), .krml files (the result of F* dumping its AST for KaRaMeL), .cm* files (OCaml build), etc.
hints: F* hint files, i.e. serialized Z3 unsat-cores that facilitate proof replay
dist: a distribution, i.e. a self-contained set of C files for clients to consume and check into their project.
tests: hand-written C tests to make sure the generated code has a suitable API.

This toy project will thus illustrate mixing hand-written and generated ML and C files, a situation that is fairly common when working in Low*. Of course, your project might not need such complexity, in which case you should feel free to simplify.

Build¶

Build is essential! Running make is the entry point for any contributor to your project. A poorly designed build system will generate frustration, angst and conflict in the project, while a well-ironed and smoothed-out build system will ensure bliss and happiness. Do not neglect your build system!

Reading, understanding and mastering the build of your project might make all the difference in the world. This section gives an overview of how we build Low* projects, followed by a reference Makefile.

Overview of a build¶

We advocate the usage of Makefiles (GNU), mostly because F* supports directly generating a .depend that will contain all the build rules for you. This is a well-debugged build system, used everywhere in Everest. It’s also easy to use, in that it only requires GNU make.

From a high-level perspective, the following steps need to happen in order to sucessfully build a Low* project:

dependency analysis of all F* source files, generating a .depend
verify all the source files for this project, generating .checked files
extract F* code using those checked files to either .krml or .ml
build and link ML code (for specs)
run KaRaMeL and generate C code
dependency analysis for the generated C code
build C code, generating a C library (more rarely, an executable)
build C tests and link against compiled library.

To limit the amount of complexity, we only recursively execute make when a new dependency analysis needs to be performed. This means that C code compilation will be a sub-make, but everything is tied together in a single Makefile. In short, our Makefile has only two stages.

Note

As a point of comparison, the HACL* Makefile has more stages: an initial one that runs the Vale tool to generate F* files, a second stage (F* compilation & extraction to C), a third stage (compilation of generated C code and ctypes bindings generation code), a fourth stage (execution then compilation of the generated Ctypes OCaml bindings), and perhaps a few more.

Interestingly enough, F* generates in a single pass enough information in the .depend to build your F* project, but also (roughly) enough information to build the resulting extracted OCaml files. This means that we do not need to rely on ocamldep to generate a dependency graph for building the extracted OCaml files.

Note

You could conceivably extract all the .ml files to a separate directory and use an external build tool, e.g. dune – this is not covered here

Separate F* builds¶

Each project is expected to build its own .checked files; running make in FStar/ establishes the invariant that all the checked files are up-to-date w.r.t. their respective source files; similarly, running make in karamel/ ensures that all the krmllib (C support libraries) .checked files are up-to-date.

Any Low* program will need to refer to both ulib in F* and krmllib in KaRaMeL. The client Makefile we provide will therefore enforce that all the checked files for the projects it depends on be up-to-date, and will error out otherwise.

The rationale is that the client project should not need to know how to build F* .checked files: there may be magic command-line flags, particular options, and special rules involved in the production of those checked files (for ulib, there are). If, say, ulib/.cache/LowStar.Comment.fst.checked is out-of-date, then the user needs to rebuild F*.

Reference Makefile¶

I now provide a reference build system (authored with GNU make) that contains more comments than actual code. It describes a very comprehensive scenario in which:

you need to mix hand-written and karamel-generated C files to produce a C library libbignum.a
you need to extract the specs to OCaml for spec testing, with a hand-written test driver;
you have hand-written C tests.

Of course this should be simplified if you’re not relying on all these features. This build is under Everest CI and will remain up-to-date.

The first Makefile defines just enough to compute the arguments to the interactive mode:

# This Makefile may be included from any sub-directory, provided BIGNUM_HOME is
# suitably defined, in order to define the %.fst-in and %.fsti-in targets for
# computing the arguments to the interactive mode.

BIGNUM_HOME ?= .

# Where is F* ?
ifndef FSTAR_HOME
  FSTAR_EXE=$(shell which fstar.exe)
  ifneq ($(FSTAR_EXE),)
    # Assuming that fstar.exe is in some ..../bin directory
    FSTAR_HOME=$(dir $(FSTAR_EXE))/..
  else
    $(error "fstar.exe not found, please install FStar")
  endif
endif
export FSTAR_HOME

ifeq (,$(KRML_HOME))
  $(error KRML_HOME is not defined)
endif

# I prefer to always check all fst files in the source directories; otherwise,
# it's too easy to add a new file only to find out later that it's not being
# checked. Note the usage of BIGNUM_HOME
SOURCE_DIRS = $(BIGNUM_HOME)/code $(BIGNUM_HOME)/specs

# We want our source tree on the include path, along with pre-built ulib and
# krmllib so that F* can reuse these build artifacts rather than reverify F* and
# krmllib as part of this build (which would be doomed to fail since there's a
# lot of trickery involved in building ulib -- better leave it up to the F*
# build!).
#
# Also note that we have our own directory on the include path for the sake of
# the interactive mode, for finding checked files for our own F* files.
INCLUDE_DIRS = \
  $(SOURCE_DIRS) \
  $(KRML_HOME)/krmllib \
  $(BIGNUM_HOME)/obj


FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))

%.fst-in %.fsti-in:
	@echo $(FSTAR_INCLUDES)

This allows authoring a minimalistic Makefile for sub-directories, whose sole purpose is to compute include paths for the interactive mode:

BIGNUM_HOME=..

include $(BIGNUM_HOME)/Makefile.include

See note above regarding the customization for the fstar-mode.el that you absolutely should have.

The top-level Makefile combines everything together. Note that, at this stage, the jury is still out as to whether you should rely on the F*-generated .depend to perform OCaml compilation, or fork out the build of the extracted OCaml code to an external tool (e.g. Dune). The latter is simpler but you lose parallelism in your build quite significantly, since extraction & compilation of OCaml can no longer be interleaved.

#############################
# This is the main Makefile #
#############################

# This tutorial assumes you have a degree of familiarity with GNU make,
# including automatic variables such as $@, $< and $^. Some mandatory reading if
# you are not fluent in GNU make:
# - https://www.gnu.org/software/make/manual/html_node/Automatic-Variables.html#Automatic-Variables
# - https://www.gnu.org/software/make/manual/html_node/Pattern-Intro.html#Pattern-Intro
# - https://www.gnu.org/software/make/manual/html_node/Pattern_002dspecific.html#Pattern_002dspecific

# I usually prefer to rule out OSX make on the basis that it doesn't have the
# shortest stem rule, which is incredibly useful.
ifeq (3.81,$(MAKE_VERSION))
  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
    install make, then invoke gmake instead of make)
endif


# Main entry points (first one is default)
# ----------------------------------------

all: dist/libbignum.a

test: tests/c-tests.test obj/specs-test.test

%.test: %.exe
	$<

include Makefile.include

# Definition of F* flags
# ----------------------

FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints

# This flag controls what gets extracted to OCaml. Generally, we don't extract
# the FStar namespace since it's already extracted and packaged as the ocamlfind
# package fstar.lib. Here, unlike in -bundle, +Spec matches both Spec and
# Spec.*
FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'

# Some reasonable flags to turn on:
# - 247: checked file not written because some of its dependencies...
# - 285: missing or file not found, almost always something to act on
# - 241: stale dependencies, almost always a sign that the build is incorrect
#
# But also:
# - --cmi, for cross-module inlining, a must-have for anyone who relies on
#   inline_for_extraction in the presence of interfaces
# - --cache_checked_modules to rely on a pre-built ulib and krmllib
# - --cache_dir, to avoid polluting our generated build artifacts outside o

# Where is F* ?
ifndef FSTAR_HOME
  FSTAR_EXE=$(shell which fstar.exe)
  ifneq ($(FSTAR_EXE),)
    # Assuming that fstar.exe is in some ..../bin directory
    FSTAR_HOME=$(dir $(FSTAR_EXE))/..
  else
    $(error "fstar.exe not found, please install FStar")
  endif
endif
export FSTAR_HOME

FSTAR_NO_FLAGS = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_HINTS) \
  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
  --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
  --cache_dir obj --hint_dir hints

# Initial dependency analysis
# ---------------------------

# Important to wildcard both fst and fsti since there are fstis without fsts,
# etc. Note that I'm using wildcard rather than assume $(SHELL) is bash and has
# fancy globbing rules -- particularly true on Windows.
FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
  $(wildcard $(addsuffix /*.fst,$(SOURCE_DIRS))) \


# This is the only bulletproof way that I know of forcing a regeneration of the
# .depend file every single time. Why, you may ask? Well, it's frequent enough
# to add a new file that you don't want to decipher a cryptic error only to
# remember you should run `make depend`. Also, if you move files around, it's
# good to force regeneration even though .depend may be more recent than the
# mtime of the moved files.
ifndef MAKE_RESTARTS
.depend: .FORCE
	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@

.PHONY: .FORCE
.FORCE:
endif

include .depend

# Verification
# ------------

# Everest-specific idiom: all makefiles accept OTHERFLAGS, for instance, if one
# wants to rebuild with OTHERFLAGS="--admit_smt_queries true". We just don't
# pass such flags to the dependency analysis.
FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS)

# Creating these directories via a make rule, rather than rely on F* creating
# them, as two calls to F* might race.
hints:
	mkdir $@

obj:
	mkdir $@

# We allow some specific pattern rules to be added here, relying on the shortest
# stem rule for them to take precedence. For instance, you may want to do:
#
# obj/Bignum.Impl.fst.checked: FSTAR_FLAGS = "--query_stats"
#
# (Note: for options that control the SMT encoding, such as
# --smtencoding.nl_arith_repr native, please make sure you also define them in
# Makefile.common for %.fst-in otherwise you'll observe different behaviors
# between interactive and batch modes.)
#
# By default, however, variables are inherited through the dependencies, meaning
# that the example above would normally set these FSTAR_FLAGS for any .checked
# that is rebuilt because it's a dependency of Bignum.Impl.fst.checked.
#
# To avoid this unpleasant behavior, the most general pattern rule (longest
# stem) also defines a suitable default value for FSTAR_FLAGS.
%.checked: FSTAR_FLAGS=

# Note: F* will not change the mtime of a checked file if it is
# up-to-date (checksum matches, file unchanged), but this will confuse
# make and result in endless rebuilds. So, we touch that file.
%.checked: | hints obj
	$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@

# Extraction
# ----------

# A few mismatches here between the dependencies present in the .depend and the
# expected F* invocation. In .depend:
#
# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
#
# But F* wants (remember that F* searches for source files anywhere on the
# include path):
#
# fstar Bignum.Impl.fst --extract_module BigNum.Impl
#
# We use basename because we may also extract krml files from .fsti.checked
# files (not true for OCaml, we don't extract mlis from fstis).
.PRECIOUS: obj/%.ml
obj/%.ml:
	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
	--extract_module $(basename $(notdir $(subst .checked,,$<)))

.PRECIOUS: obj/%.krml
obj/%.krml:
	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
	--extract_module $(basename $(notdir $(subst .checked,,$<)))

obj/Specs_Driver.ml: specs/ml/Specs_Driver.ml
	# This ensures that all the source directories are not polluted with
	# build artifacts
	cp $< $@

# F* --> C
# --------

KRML=$(KRML_HOME)/krml

# Note: the implementation of the intrinsic uses external linkage, but you could
# easily turn this file into a .h, use -add-include '"Impl_Bignum_Intrinsics.h"'
# and pass -static-header Impl.Bignum.Intrinsics as described in the
# documentation.
HAND_WRITTEN_C_FILES = code/c/Impl_Bignum_Intrinsics.c

# This is now the preferred and recommended way to compile C code with KaRaMeL.
#
# KaRaMeL (via -skip-compilation) only generates a stub Makefile in dist/,
# instead of acting as a C compilation driver like it did before. The Makefile
# that is generated by KaRaMeL is basic, but takes into account:
# - the -o option to determine what is being built
# - the C files passed on the command line, which will be linked together
# - C compiler flags passed to KaRaMeL via -ccopts
#
# This Makefile is called Makefile.basic and should be enough for all your basic
# needs. If you need something more fancy, you can easily author your own custom
# dist/Makefile, which includes Makefile.basic, then proceeds to redefine /
# tweak some variables.
#
# Note that you are of course more than welcome to define your own
# CMakeLists.txt or whatever your favorite build system is: this tutorial only
# describes the supported canonical way of compiling code.
#
# See the advanced topics section for an in-depth explanation of how the -bundle
# option works. We also use -minimal.
dist/Makefile.basic: $(filter-out %prims.krml,$(ALL_KRML_FILES)) $(HAND_WRITTEN_C_FILES)
	mkdir -p $(dir $@)
	cp $(HAND_WRITTEN_C_FILES) $(dir $@)
	$(KRML) -tmpdir $(dir $@) -skip-compilation \
	  $(filter %.krml,$^) \
	  -warn-error @4@5@18 \
	  -fparentheses \
	  -bundle Impl.Bignum.Intrinsics= \
	  -bundle 'LowStar.*,Prims' \
	  -bundle Impl.Bignum=Impl.Bignum.*,Spec.*[rename=Bignum] \
	  -minimal \
	  -bundle 'FStar.*' \
	  -add-include '<stdint.h>' \
	  -add-include '"krml/internal/target.h"' \
	  $(notdir $(HAND_WRITTEN_C_FILES)) \
	  -o libbignum.a

# Compiling the generated C code
# ------------------------------

# Here we do a recursive make invocation because a new dependency analysis needs
# to be performed on the generated C files. This recursive make deals with all
# the files copied in dist, which includes karamel-generated and hand-written,
# copied files from HAND_WRITTEN_C_FILES.

dist/libbignum.a: dist/Makefile.basic
	$(MAKE) -C $(dir $@) -f $(notdir $<)

# Compiling the generated OCaml code
# ----------------------------------

# This is much more difficult, and you're probably better off calling OCamlbuild
# or Dune at this stage. Nonetheless, I still show how to compile the generate
# OCaml code with only GNU make and without relying on an external tool or an
# extra dependency analysis.

# First complication... no comment.
# NOTE: if F* was installed via opam, then this is redundant
ifeq ($(OS),Windows_NT)
  export OCAMLPATH := $(FSTAR_HOME)/lib;$(OCAMLPATH)
else
  export OCAMLPATH := $(FSTAR_HOME)/lib:$(OCAMLPATH)
endif

# Second complication: F* generates a list of ML files in the reverse linking
# order. No POSIX-portable way of reversing the order of a list.
TAC = $(shell which tac >/dev/null 2>&1 && echo "tac" || echo "tail -r")

ALL_CMX_FILES = $(patsubst %.ml,%.cmx,$(shell echo $(ALL_ML_FILES) | $(TAC)))

# Third complication: F* does not know about our hand-written files. So, we need
# to manually add dependency edges in the graph. In our case, the test driver
# needs all files to be built before. This is convenient because the
# hand-written file only needs to be inserted at the end of the list of CMX
# files. If it had to be inserted somewhere in the middle of the topological
# order, it would be trickier...

obj/Specs_Driver.cmx: $(ALL_CMX_FILES)

# Finally, how to compile things...

OCAMLOPT = ocamlfind opt -package fstar.lib -linkpkg -g -I $(BIGNUM_HOME)/obj -w -8-20-26

.PRECIOUS: obj/%.cmx
obj/%.cmx: obj/%.ml
	$(OCAMLOPT) -c $< -o $@

obj/specs-test.exe: $(ALL_CMX_FILES) obj/Specs_Driver.cmx
	$(OCAMLOPT) $^ -o $@

# Compiling the hand-written test
# -------------------------------

CFLAGS += -I dist -I $(KRML_HOME)/include

tests/c-tests.exe: dist/libbignum.a tests/c-tests.o
	$(CC) $^ -o $@