Introduction

This manual documents Low*, a subset of F* that enjoys compilation to C through its companion compiler KreMLin. As such, KreMLin offers an alternative to OCaML for extracting and running F* programs (hence the name – also a pun on K&R C).

Low* is not only a language subset, but also a set of F* libraries that model a curated set of C features: the C memory model, stack- and heap-allocated arrays, machine integers, C string literals, and a few system-level functions from the C standard library.

Writing in Low*, the programmer enjoys the full power of F* for proofs and specifications. At compile-time, proofs are erased, leaving only the low-level code to be compiled to C. In short:

the code is low-level, but the verification is not.

This manual offers a tour of Low* and its companion libraries; presents the KreMLin tool and the various ways it can be used to generate C programs or libraries; covers a few advanced examples.

Low* has been successfully used to write numerous projects, including:

  • HACL*, a library of verified cryptographic primitives used in Firefox, the Linux Kernel and other projects;
  • EverCrypt, a multiplexing, agile, abstract cryptographic provider that combines C and ASM implementations of state-of-the art cryptographic algorithms;
  • EverQuic, an implementation of the QUIC packet encryption and decryption,
  • EverParse, a library of low-level, zero-copy validators and serializers for parsing binary message formats.

This tutorial assumes the reader is familiar with F*; when in doubt, head over to its tutorial. For a research-oriented perspective on Low*, see the initial ICFP’17 paper and subsequent application papers on the publications page.

The essence of Low*

Consider the following very simple program:

module Intro

module P = LowStar.Printf
module C = LowStar.Comment
module B = LowStar.Buffer

open FStar.HyperStack.ST
open LowStar.BufferOps

let main (): St Int32.t =
  push_frame ();
  let b: B.buffer UInt32.t = B.alloca 0ul 8ul in
  b.(0ul) <- 255ul;
  C.comment "Calls to printf are desugared via meta-programming";
  let s = "from Low*!" in
  P.(printf "Hello from %s\nbuffer contents: %xul\n"
    s 8ul b done);
  pop_frame ();
  0l

Leaving an in-depth explanation of the code to subsequent sections, suffices to say, for now, that this code demonstrates:

  • authoring a main function that operates within the special C-like memory model, called HyperStack.St, which accounts for stack-based and heap-based memory management;
  • executing a piece of code within a fresh stack frame (push_ and pop_frame), reflecting the structure of the call stack using F*’s built-in effect system
  • dealing with C-like machine integers (UInt32.t and the 0ul literal syntax for 32-bit unsigned integers), which are accurately modeled in F* to account for the underlying C behavior (e.g. no signed overflow)
  • using the Buffer library which models C arrays, offering stack (alloca) and heap-based allocations; the library enforces temporal and spatial safety, relying on an accurate model of the C standard (e.g. no pointer addition unless the base pointer is live);
  • generating comments into the resulting C source code (C.comment)
  • using the LowStar.Printf library to meta-program a series of stateful calls using a printf-like combinator, evaluated within F*.

Once compiled by the KreMLin compiler, we obtain the following C code:


int32_t main()
{
  uint32_t b[8U] = { 0U };
  b[0U] = (uint32_t)255U;
  /* Calls to printf are desugared via meta-programming */
  Prims_string s = "from Low*!";
  LowStar_Printf_print_string("Hello from ");
  LowStar_Printf_print_string(s);
  LowStar_Printf_print_string("\nbuffer contents: ");
  LowStar_Printf_print_lmbuffer_u32((uint32_t)8U, (uint32_t *)b);
  LowStar_Printf_print_string("\n");
  return (int32_t)0;
}

Once compiled by a C compiler, the output is as follows:

Hello from from Low*!
buffer contents: ff 0 0 0 0 0 0 0

Structure of this manual

The goal of this manual is to provide both:

  • a user’s guide to getting started with Low* and the toolchain, setting up a project, its build, the interactive mode, and providing pointers for idiomatic examples of how to author code in Low*
  • an advanced guide, on how to achieve separate builds, the integration of hand-written and auto-generated code, generating static headers, dangers of doing so, how to achieve abstraction and modularity in Low*v2, etc.
  • a reference manual for the krml tool, including code-generation options and tweaks
  • a library reference, for all the modules in the LowStar namespace
  • a repository of tips-and-tricks for larger projects, including how to author robust proofs, selectively overriding ifuel settings using allow_inversion, dangerous patterns to be aware of, etc.