Reference — Overview

The tutorial teaches C* by working through programs. It introduces one idea at a time, in an order chosen so that each step is motivated by the step before it, and it happily postpones details that would get in the way of the story.

This reference does the opposite. It states what is true, arranged so that things are easy to find rather than easy to follow, and it assumes you already know why you are looking. No page here builds an argument; every page is a place to land. 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, and most reference questions are really questions about which of the three you are currently writing. Identifying the layer is usually enough to identify the page.

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 is what those terms mean. A well-formed assertion denotes a predicate over memory, and the proof steps you take on it are governed by 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 proved from the primitive laws or taken as an axiom. These 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 it return, 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, the reference is the wrong door. Start at Getting Started, follow the tutorial until the shape of a verified function is familiar, and come back here when you want the details it left out.