Reference — Overview

The tutorial teaches C* by working through programs. It introduces one idea at a time, with each step motivated by the previous one, and postpones details that would interrupt the explanation.

This reference states the facts and organizes them for lookup, assuming you already know what you need to find. Each page can be consulted directly without following a step-by-step argument. Consult it when you need the exact syntax accepted inside backticks, the exact statement of a rule you are about to apply, or the exact C signature of a function your proof block calls.

A C* source file mixes three languages. Most reference questions concern the language you are currently writing. Identifying the layer usually tells you which page to consult.

The logic level is everything between backticks — the assertions inside [[cst::require(...)]][[cst::require(...)]], [[cst::ensure(...)]][[cst::ensure(...)]], and [[cst::invariant(...)]][[cst::invariant(...)]], and the terms passed to proof functions. This text is not C: it is parsed by HOL Light’s term parser, extended with C*-specific constants and notation. Questions at this level are lexical and grammatical — which identifiers are reserved, how an operator associates, what the ii in 0i0i means, which type a constant has. They are answered by Logic-Level Syntax.

The assertion level concerns the meaning of those terms. A well-formed assertion denotes a predicate over memory, and proof steps on it follow the rules of separation logic: which states satisfy data_at p Tint vdata_at p Tint v, what **** demands of the two halves it joins, which rule lets you discard a conjunct, and whether a given rule is a primitive law or a consequence of primitive laws. These questions are answered by Separation Logic.

The implementation level is ordinary C. Proof blocks are compiled C code, and everything they do — building a term, applying an inference rule, reading the symbolic state, discharging a verification condition — is a call to a function declared in the headers that ship with the toolchain. Questions here are the usual ones about a C API: what is the signature, what does the function return, and what does it do on failure? They are answered by Kernel Headers.

If you have not installed the toolchain or written a C* file yet, start at Getting Started, follow the tutorial until the structure of a verified function is familiar, and return here when you want the details it left out.