Introduction¶
This manual documents Low*, a subset of F* that enjoys compilation to C through its companion compiler KaRaMeL. As such, KaRaMeL 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 KaRaMeL 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, calledHyperStack.St
, which accounts for stack-based and heap-based memory management; - executing a piece of code within a fresh stack frame (
push_
andpop_frame
), reflecting the structure of the call stack using F*’s built-in effect system - dealing with C-like machine integers (
UInt32.t
and the0ul
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 KaRaMeL compiler, we obtain the following C code:
int32_t main(void)
{
uint32_t b[8U] = { 0U };
b[0U] = 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(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.