Setup F* on Linux

HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C. ValeCrypt provides formally proven implementations of cryptographic primitives in Vale, a framework for verified assembly language programming embedded in F*. EverCrypt combines them into a single cryptographic provider. Code from these projects is now used in production in several projects, including Mozilla Firefox, the Linux kernel, Python, mbedTLS, the Tezos blockchain, the ElectionGuard electronic voting SDK, and the Wireguard VPN.

EverParse is a parser generator for binary formats that produces C code extracted from formally proven F*. Parsers from EverParse are used in production in several projects, including in Windows Hyper-V, where every network packet passing through the Azure cloud platform is parsed and validated first by code generated by EverParse. EverParse is also used in other production settings, including ebpf-for-windows.

First, install F* with its dependencies in your $HOME:

curl -fsSL https://aka.ms/install-fstar | bash -s -- --release

Then build the missing library:

cd ~/.local/fstar/lib/krml/dist/generic
# Check such line, it must exist:
grep -n "libkrmllib" Makefile.basic
# If yes, then let's build the library:
make -f Makefile.basic
# Now check that it was built:
ls -l libkrmllib.a

Create some a directory for your project. Then, inside it we should build a directory structure like:

p1/                        <-- this is my project's directory
├── Makefile
├── fstar/
│   └── Simple.fst
├── c/
│   └── main.c
└── build/
    ├── cache/
    └── out/

So:

mkdir -p build/{cache,out}
mkdir c fstar

Put in fstar/ folder a file Simple.fst:

module Simple
open FStar.UInt32

let square (x:UInt32.t) : UInt32.t =
  x *%^ x

Put in c/main.c file this code:

#include <stdint.h>
#include <stdio.h>
#include "Simple.h"

int main(void)
{
    uint32_t x = 12;
    uint32_t y = Simple_square(x);
    printf("square(%u) = %u\n", x, y);
    return 0;
}

FSTAR := fstar.exe
KRML  := krml

BUILD := build
CACHE := $(BUILD)/cache
OUT   := $(BUILD)/out

FSTAR_SRC := fstar/Simple.fst
KRML_SRC  := $(OUT)/out.krml

.PHONY: all clean

all: $(BUILD)/demo

$(BUILD):
        mkdir -p $(BUILD)

$(CACHE):
        mkdir -p $(CACHE)

$(OUT):
        mkdir -p $(OUT)

# 1. Verify the F* module
$(CACHE)/Simple.fst.checked: $(FSTAR_SRC) | $(CACHE) $(OUT)
        $(FSTAR) \
                --cache_checked_modules \
                --cache_dir $(CACHE) \
                --odir $(OUT) \
                --ext fly_deps=false \
                $(FSTAR_SRC)

# 2. F* -> KaRaMeL .krml
$(KRML_SRC): $(CACHE)/Simple.fst.checked
        $(FSTAR) \
                --cache_checked_modules \
                --cache_dir $(CACHE) \
                --odir $(OUT) \
                --ext fly_deps=false \
                --codegen krml \
                $(FSTAR_SRC)

# 3. KaRaMeL -> C -> executable
$(BUILD)/demo: $(KRML_SRC) c/main.c
        $(KRML) \
                -tmpdir $(OUT) \
                $(KRML_SRC) \
                c/main.c \
                -o $(BUILD)/demo

clean:
        rm -rf $(BUILD)

Return to the project's directory and build the project with make command (just type make). You will get now this structure:

build
├── cache
│   └── Simple.fst.checked      <-- result of proving
├── demo*                       <-- executable file (from main.c)
└── out
    ├── compile_flags.txt
    ├── main.o
    ├── Makefile.basic
    ├── Makefile.include
    ├── out.krml
    ├── Simple.c                <-- generated C code
    ├── Simple.h                <-- C header file for API
    └── Simple.o

F* checked the code (well, current code is primitive kiddish code, nothing to prove there, currently, but this is a skeleton only), then it used the result of checking and it "extracted" (this is the term, not "translated") C code (Simple.c, Simple.h) and, finally, it called gcc compiler which produced demo binary file. It is small, 21752 bytes, because it's a result of usual C code compiled by gcc.

The resulting extracted C code is also super-simple:

/*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  KaRaMeL invocation: krml -tmpdir build/out build/out/out.krml c/main.c -o build/demo
  F* version: <unknown>
  KaRaMeL version: 9abbb865b10a0cd5c557da81c024c3965cb6ff53
 */

#include "Simple.h"

uint32_t Simple_square(uint32_t x)
{
  return x * x;
}

It is not always so simple and plain, but usually it is. Actually, it depends on the complexity of the input F* code.

The workflow is:

                  Simple.fst
                      |
                      | F* verification
                      v
             Simple.fst.checked
                      |
                      | F* extraction
                      v
                  out.krml
                      |
                      | KaRaMeL
                      v
                Simple.c/.h
                      |
                      | GCC
                      v
                     demo
                      | output on stdout
                      v
              square(12) = 144

KaRaMeL is the "extractor", other extractions are also supported:

Various fragments of F* can also be extracted to F#, to C or Wasm by a tool called KaRaMeL, or to assembly using the Vale toolchain. F* is implemented in F* and bootstrapped using OCaml.