C* Extensions

The previous page described the syntax C* inherits unchanged from HOL Light. This page lists C*‘s extensions: type constants for expressing separation logic and C types, the constants and notations built from them, and naming conventions that connect logical variables to the C program being verified.

The constructs listed here appear inside backtick-quoted logical expressions. The entries describe syntax and types: each name, its type, and how to read it. The meaning of the separation-logic constants is given in Memory Model and Assertions, and the memory predicates are developed in Typed Memory Predicates.

C* introduces four type constants into HOL Light’s type language. They follow the type syntax described on the previous page and may appear wherever a type is allowed, including annotations such as (x:addr)(x:addr) and postfix constructor applications such as (hprop)list(hprop)list.

struct_namestruct_name and fieldfield are declared as bare 0-ary type constants without constructors. The library predeclares no program-specific struct-name or field-name constants; a program introduces its own, as described under “Structs and Fields” below. ctypectype is an inductive type; its constructors are listed in the section on C types. hprophprop is the type of assertions; in C*‘s shallow embedding it unfolds to a predicate over memory, but at the level of syntax it behaves as an opaque type constant.

Two type abbreviations name the roles that integers play in the memory model:

addr = :int
byte = :int

addr = :int
byte = :int

Type abbreviations are transparent: addraddr and intint are the same type, and the type checker does not distinguish them. The abbreviations document the arguments’ roles: the signature addr->ctype->int->hpropaddr->ctype->int->hprop distinguishes the address from the stored value, whereas int->ctype->int->hpropint->ctype->int->hprop does not.

An unsuffixed numeral is a natural number; C* extends the lexer so that a numeral with the suffix ii is an integer.

C* models addresses, stored values, sizes, and offsets as integers of type intint, so nearly every numeral in a C* assertion carries the ii suffix. Dropping it is the most common type error when writing assertions:

data_at p Tint 42data_at p Tint 42

fails to type-check, because data_atdata_at expects an intint and 4242 is a numnum.

Negation of a literal is the prefix ----, not --: the additive inverse of 1i1i is --(1i)--(1i), since -- is reserved for binary subtraction.

The constants below form the separation-logic vocabulary. The first group builds assertions and has result type hprophprop; the last group states relations between assertions and has result type boolbool. Thus, p |-- qp |-- q is a proposition about two assertions, not an assertion itself.

existsexists and forallforall are binders: they are written

exists x. pexists x. p

and

forall x y. pforall x y. p

, as syntactic sugar for applying the constant to a lambda abstraction. The type variable AA in their signatures is unconstrained: one may quantify over an intint, an addraddr, a list, or any other type.

Six of these names are overloaded: in addition to their hprophprop versions, truetrue, falsefalse, existsexists, forallforall, &&&&, and |||| each have a Boolean counterpart. Type inference selects the appropriate one from context. In

fact(x > 0i && y > 0i)fact(x > 0i && y > 0i)

the &&&& is Boolean conjunction (HOL Light’s /\/\); in

fact(x > 0i) && empfact(x > 0i) && emp

it is heap conjunction. By contrast |--|--, -|--|-, -||--||-, -*-*, -->-->, ****, empemp, purepure, and factfact are C*-specific names with no Boolean interpretation. C* conventionally uses different notation for the two quantifier layers: the boolbool layer uses the symbols !! and ??, the hprophprop layer the words forallforall and existsexists.

The three relational notations must be distinguished. -|--|- is HOL Light’s equality at type hprophprop, that is (=):hprop->hprop->bool(=):hprop->hprop->bool under another name; theorem statements about assertions are printed with this notation. Thus, a representation predicate’s definition is written with == but printed with -|--|-. -||--||- is a separately defined constant, logic_equivlogic_equiv, meaning entailment in both directions. The two agree extensionally, but they are distinct terms, and a rule stated with one does not match a goal written with the other; the library’s rules are stated with -|--|-.

For the precedence and associativity of all these infixes see the operator table in HOL Light Syntax for their definitions and the laws they satisfy see Memory Model and Assertions.

These constants form assertions that describe C memory. Each takes an address, a ctypectype specifying how to read the memory, and a description of its contents.

Argument order for the segment forms is: address, C type, then the indices, then (for the initialized family only) the contents list. The missing_imissing_i forms take the removed index first among the indices, as in array_at_missing_i_rec x ty i lo hi larray_at_missing_i_rec x ty i lo hi l. The undef_undef_ family carries no contents list, since there is nothing to say about the value of uninitialized memory; the index arguments are otherwise parallel, with a trailing length argument in place of the list.

Element ii of an array based at xx is at address x + i * sizeof(ty)x + i * sizeof(ty), which is exactly the address C* produces when it elaborates the C subscript expression a[i]a[i]. For the rules for splitting, merging, and rebasing these predicates, see Typed Memory Predicates.

A value of type ctypectype represents a C type in the logic: it tells data_atdata_at how many bytes a location occupies and which values it may hold. Nine constructors cover the scalar types C* models. Compound C types also have constructors; the logic interprets TaliasTalias through its underlying type and treats the others as opaque.

TptrTptr represents every pointer type. The logic does not record the type of the pointed-to object, so int *int * and struct list *struct list * are both TptrTptr.

The compound C types are represented but not modelled:

Tstruct string | Tenum string | Tunion string |
Talias string ctype | Tarray int ctype |
Tfun (string)list (ctype)list ctype

Tstruct string | Tenum string | Tunion string |
Talias string ctype | Tarray int ctype |
Tfun (string)list (ctype)list ctype

TstructTstruct, TenumTenum and TunionTunion carry only the tag name; Talias name tyTalias name ty is a typedeftypedef, and the functions below use its underlying type; Tarray n tyTarray n ty is an array of nn elements; TfunTfun records a function signature (parameter names, parameter types, result type) and occurs only inside the function-pointer specifications fnspecfnspec and fnspec_wfnspec_w described on Typed Memory Predicates. Hand-written assertions use the nine scalar constants and access struct memory through field_addrfield_addr.

Three functions extract information from a ctypectype:

Struct and field names are represented in the logic by constants of the dedicated types struct_namestruct_name and fieldfield. The library predeclares no program-specific name constants of either type; a program introduces the ones it needs, typically with new_constnew_const in a global proof declaration. The naming convention is that a struct-name constant is the C struct name prefixed with TT, and a field-name constant is the C field name prefixed with FF — struct liststruct list becomes TlistTlist, and its fields headhead and tailtail become FheadFhead and FtailFtail. C* uses these names to match the C program with its logical representation, so the prefixes are required.

Field addresses are computed by two constants:

field_offset : struct_name->field->int
field_addr   : addr->struct_name->field->addr

field_offset : struct_name->field->int
field_addr   : addr->struct_name->field->addr

field_offsetfield_offset is a primitive constant declared without a definition: the byte offsets for a struct are left uninterpreted and supplied to the verifier for each program. field_addrfield_addr has a definition whose theorem is registered in the theorem database as field_addr_propfield_addr_prop:

field_addr x s f = x + field_offset s f

field_addr x s f = x + field_offset s f

So field_addr pt Tlist Ftailfield_addr pt Tlist Ftail denotes the address of the tailtail field of the struct liststruct list at ptpt, and nested accesses compose: the C expression &it->node.next&it->node.next becomes field_addr (field_addr it Titem Fnode) Tlink Fnextfield_addr (field_addr it Titem Fnode) Tlink Fnext.

C’s bitwise operators are not primitive in the logic. C* defines four families over intint, for signed and unsigned integers at 32 and 64 bits, using the machine-word semantics of HOL Light’s word library.

Each operator is an ordinary HOL definition, not an axiom. Its defining theorem is available from the theorem database under the name <op>_def<op>_def. The definitions convert value operands to N-bit words with iwordiword: both operands for bitwise and, or, and exclusive or, the single operand for complement, and the value being shifted for shifts. Shift counts are converted with num_of_intnum_of_int. After applying the word operation, the result is converted back to an integer using ivalival (signed interpretation) for the i32_i32_/i64_i64_ family and &(val ...)&(val ...) (unsigned interpretation) for the u32_u32_/u64_u64_ family.

i32_and x y = ival (word_and ((iword x):(32)word) ((iword y):(32)word))
u32_and x y = &(val (word_and ((iword x):(32)word) ((iword y):(32)word)))
i64_shr x y = ival (word_ishr ((iword x):(64)word) (num_of_int y))
u64_shr x y = &(val (word_ushr ((iword x):(64)word) (num_of_int y)))

i32_and x y = ival (word_and ((iword x):(32)word) ((iword y):(32)word))
u32_and x y = &(val (word_and ((iword x):(32)word) ((iword y):(32)word)))
i64_shr x y = ival (word_ishr ((iword x):(64)word) (num_of_int y))
u64_shr x y = &(val (word_ushr ((iword x):(64)word) (num_of_int y)))

Two details of this encoding matter when reasoning about these operators.

• Value operands wrap for every integer. iwordiword is defined on every integer, including negative integers, so u32_and (a - b) cu32_and (a - b) c is well specified even when b > ab > a. The model keeps intermediate results of unsigned C arithmetic as mathematical integers and has no u32_subu32_sub; a partial encoding would leave such terms unsimplifiable.
• Negative shift counts are unspecified. The second operand of shlshl and shrshr passes through num_of_intnum_of_int, which is unspecified on negative inputs. This is consistent with C’s undefined behaviour for negative shift counts. A proof that evaluates a shift must establish that the count is non-negative.

Right shift also depends on signedness at the word level: the signed family uses the arithmetic shift word_ishrword_ishr, the unsigned family the logical shift word_ushrword_ushr.

Two further operators model C’s conversion of a value to a given bit width:

signed_last_nbits   x y = cast_signed y x
unsigned_last_nbits x y = cast_unsigned y x

signed_last_nbits   x y = cast_signed y x
unsigned_last_nbits x y = cast_unsigned y x

Both have type int->int->intint->int->int, where xx is the value and yy the target width in bits. The argument order is the reverse of that used by cast_signedcast_signed and cast_unsignedcast_unsigned in the C-semantics layer. cast_unsigned n zcast_unsigned n z is z rem exp_2 nz rem exp_2 n (HOL’s remrem is Euclidean, so the result is never negative), and cast_signedcast_signed adjusts the residue to lie in the signed range. Both are total and work across bit widths: they handle negative xx and widths of 64 bits and beyond.

The following three facts have been proved and are available from the theorem database:

The _range_range lemmas give the range of the result and can discharge a data_atdata_at range obligation after a conversion. unsigned_last_nbits_idunsigned_last_nbits_id states that conversion preserves a value already in range. Its premise is exactly the condition under which the C* frontend removes a conversion from a verification condition. The definitions of cast_signedcast_signed and cast_unsignedcast_unsigned are themselves exported, under the names cast_signed_defcast_signed_def and cast_unsigned_defcast_unsigned_def, so a proof block can unfold these definitions when needed.

C*‘s memory model includes the store in the heap: an assertion has no notion of “program variable”, so a C variable must appear in the logic as an ordinary logical variable. The symbolic execution engine generates these variables using a fixed naming scheme, and assertions in contracts and invariants are written using exactly these names.

The separator is a double underscore. The lexer treats these names as ordinary identifiers: __ is an alphanumeric character in HOL Light, so x__addrx__addr is a single token. A program can still declare its own variable with that name, causing a naming collision.

An intint parameter xx therefore contributes the resource data_at x__addr Tint x__predata_at x__addr Tint x__pre to the symbolic state at function entry, and an uninitialized local int rint r contributes undef_data_at r__addr Tintundef_data_at r__addr Tint. The value range of x__prex__pre is part of the data_atdata_at resource, rather than a separate pure fact in the symbolic state. A proof can extract it using the range rule.

int abs_diff(int a, int b)
    [[cst::require(`emp`)]]
    [[cst::ensure(`fact(__return == a__pre - b__pre || __return == b__pre - a__pre) **
                   fact(__return >= 0i)`)]];

int abs_diff(int a, int b)
    [[cst::require(`emp`)]]
    [[cst::ensure(`fact(__return == a__pre - b__pre || __return == b__pre - a__pre) **
                   fact(__return >= 0i)`)]];

For contracts and invariants using these names, see Function Contracts, Loop Invariants, and Assertions for their use in the conditions generated by the engine, see Verification Condition Generation.

Logical expressions enter a C* program through C23 attributes in the cst::cst:: namespace. Function attributes follow the parameter list of a prototype or definition; statement attributes precede the statement they govern (a loop for the invariants, a call for wherewhere) or stand as a statement of their own. Every argument in the table below is a backtick quotation, parsed according to the rules in this group of reference pages.

Three further spellings are produced by the toolchain rather than written by hand: [[cst::include("cstar.h")]];[[cst::include("cstar.h")]]; is what a #cst_include#cst_include directive becomes after preprocessing, [[cst::module("dep.c")]];[[cst::module("dep.c")]]; is what a #require "dep.c"#require "dep.c" module dependency becomes (the name avoids a clash with the precondition attribute), and [[cst::lsp]][[cst::lsp]] is the marker the editor integration injects to dump the symbolic state at a line. The tutorial pages Function Contracts, Loop Invariants, and Assertions and Your First C* Program show these attributes in use.

• C* adds the type constants hprophprop, ctypectype, struct_namestruct_name, fieldfield to HOL Light’s type language, plus the transparent abbreviations addr = :intaddr = :int and byte = :intbyte = :int.
• A numeral is a numnum unless it carries the ii suffix, which makes it an intint; theorem statements from the library use the equivalent &n&n injection notation instead.
• The heap-proposition constants — ****, &&&&, ||||, -*-*, -->-->, empemp, purepure, factfact, truetrue, falsefalse, existsexists, forallforall — build assertions; |--|--, -|--|-, -||--||- relate assertions and have result type boolbool. Six of the names are overloaded with Boolean counterparts.
• data_atdata_at/undef_data_atundef_data_at and the array_atarray_at/undef_array_atundef_array_at families describe C memory; every signature takes a ctypectype argument, and array element ii is at x + i * sizeof(ty)x + i * sizeof(ty).
• Nine ctypectype constructors cover the scalar C types and TaliasTalias is interpreted through its underlying type; TstructTstruct, TenumTenum, TunionTunion, TarrayTarray and TfunTfun are opaque; sizeofsizeof, min_ofmin_of, max_ofmax_of extract information from the scalar types; structs enter through TT-prefixed and FF-prefixed constants together with field_addr x s f = x + field_offset s ffield_addr x s f = x + field_offset s f.
• The bitwise operators are defined over HOL’s machine words: value operands wrap for every integer via iwordiword, and shift counts pass through num_of_intnum_of_int (a negative count being C undefined behaviour). Width conversions are defined using integer remainder, and the range lemmas for signed_last_nbitssigned_last_nbits and unsigned_last_nbitsunsigned_last_nbits are proved. Neither family is axiomatized.
• Program variables reach the logic as x__addrx__addr, x__prex__pre, and __return__return.
• Quotations enter a program through the cst::cst:: attributes: paramparam, requirerequire, ensureensure on functions; invariantinvariant, partial_invariantpartial_invariant, assertassert, partial_assertpartial_assert, wherewhere, where_typewhere_type, givengiven on statements; proofproof for proof blocks and ghost declarations.