Logic-Level Syntax

A C* source file contains two languages. Outside backticks it is C, read by the C* compiler. Inside backticks — in a contract, in a global proof declaration, in an argument to a proof-kernel function — it is the logic-level language: a logical expression that denotes a HOL type or a HOL term, and that is lexed, parsed, and type-checked by the HOL Light proof assistant that C* is built on.

That inner language is HOL Light’s, not C’s. Its lexer, its precedence table, its binders, and its type inference are the ones HOL Light ships with, so a term such as `!n. n > 0i ==> ~(n = 0i)``!n. n > 0i ==> ~(n = 0i)` means in C* exactly what it means in a HOL Light session. On top of that base, C* adds type constants for verification (hprophprop, ctypectype, addraddr, bytebyte), the integer literal suffix ii, the separation-logic connectives, and a naming convention that ties logical variables to program variables.

This group is the reference for both halves: what HOL Light already gives you, and what C* adds.

HOL Light Syntax specifies the inherited base: the lexical structure (character classes, identifiers, reserved words, string literals), the type syntax (the TyvarTyvar/TyappTyapp abstract syntax, postfix type application, the ^^, ##, ++, ->-> constructors and their precedence), and the term syntax (the VarVar/ConstConst/CombComb/AbsAbs abstract syntax, the full infix precedence table, term forms such as lists, set comprehensions, matchmatch and letlet, the binders and prefixes, and how overloading and implicit types are resolved by type inference).

C* Extensions specifies what C* adds on top: the verification-oriented type constants and abbreviations, the 123i123i integer literals, the heap-proposition constants and separation-logic connectives, the typed memory predicates, the ctypectype constants together with sizeofsizeof, min_ofmin_of, max_ofmax_of, and field_addrfield_addr, the fixed-width bitwise operators, and the reserved logical variable names (x__addrx__addr, x__prex__pre, __return__return) through which the symbolic execution engine talks about program variables.