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