Skip to content

Latest commit

 

History

History
253 lines (195 loc) · 10.7 KB

Introduction.rst

File metadata and controls

253 lines (195 loc) · 10.7 KB

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:

.. centered:: **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:

.. literalinclude:: notfslit/Intro.fst
    :language: fstar

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 KaRaMeL compiler, we obtain the following C code:

.. literalinclude:: ../test/.output/Intro.out/Intro.c
    :language: c
    :start-after: SNIPPET_START: main
    :end-before: SNIPPET_END: main

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.