C* Extensions

The previous page described the syntax C* inherits unchanged from HOL Light. This page catalogues what C* adds on top of it: the type constants that make separation logic and C types expressible in the logic, the constants and notations built from them, and the naming conventions that connect logical variables back to the C program being verified.

Everything listed here lives inside the backticks of a logical expression. The entries form a syntactic and type-level catalogue — what a name is called, what type it has, how it is read. What the separation-logic constants mean 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 are ordinary members of the type syntax described on the previous page: they may appear wherever a type may, including in annotations such as (x:addr)(x:addr) and under postfix constructor application, as in (hprop)list(hprop)list.

struct_namestruct_name and fieldfield are declared as bare 0-ary type constants with no constructors at all: nothing inhabits them until a program introduces its own struct-name and field-name constants, as described under “Structs and Fields” below. ctypectype by contrast is an inductive type, whose 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

An abbreviation is transparent — addraddr and intint are the same type, and the type checker will not keep them apart. Their purpose is documentary: a signature written addr->ctype->int->hpropaddr->ctype->int->hprop says which argument is an address and which is a stored value, where int->ctype->int->hpropint->ctype->int->hprop would not.

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

C*‘s modeling of C programs is integer-valued throughout — addresses, stored values, sizes, and offsets all have type intint — so essentially 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 wants 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 are the separation-logic vocabulary. The first group builds assertions and has result type hprophprop; the last group states relations between assertions and therefore has result type boolbool — p |-- qp |-- q is not itself an assertion, but a proposition about two assertions.

existsexists and forallforall are binders: they are written

exists x. pexists x. p

and

forall x y. pforall x y. p

, which is 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 anything else.

Six of these names are overloaded rather than exclusive to hprophprop: truetrue, falsefalse, existsexists, forallforall, &&&&, and |||| each also denote a boolean counterpart, and type inference picks between them 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 reading. C*‘s convention also keeps the two quantifier layers apart notationally: the boolbool layer uses the symbols !! and ??, the hprophprop layer the words forallforall and existsexists.

The three relational notations differ in a way worth stating precisely. -|--|- is HOL Light’s equality at type hprophprop, that is (=):hprop->hprop->bool(=):hprop->hprop->bool under another name; it is what a printed theorem about assertions displays, which is why a definition of a representation predicate is written with == yet prints with -|--|-. -||--||- is a separately defined constant, logic_equivlogic_equiv, meaning entailment in both directions. The two agree extensionally, but they are distinct terms, and the library’s rules distinguish them.

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 are the assertions that describe C memory. Each takes an address, a ctypectype saying how that memory is to be read, and a description of the 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 number ii of an array based at xx sits 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]. The rules for splitting, merging, and rebasing these predicates — and the fact that the user-facing ones are supplied as axioms rather than proved from the byte-level model — are the subject of Typed Memory Predicates.

A value of type ctypectype is the logical avatar of a C type: it is what tells data_atdata_at how many bytes a location occupies and which values it may hold. Nine constants cover the scalar types C* models.

TptrTptr is uniform across pointer types — the logic does not record what a pointer points to, so int *int * and struct list *struct list * are both TptrTptr. (The ctypectype datatype carries one further constructor, TstructTstruct, used inside the library’s byte-level development; hand-written assertions use the nine scalar constants and reach struct memory through field_addrfield_addr instead.)

Three functions read information out of a ctypectype:

Struct and field names enter the logic as constants of the dedicated types struct_namestruct_name and fieldfield. The library declares no inhabitants of either type in advance; 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* matches the C program against the logic by these names, so the prefixes are load-bearing, not decorative.

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 primitive, declared with no definition: the actual byte offsets of a given struct are left uninterpreted and supplied to the verifier per program. field_addrfield_addr by contrast is defined, and its defining theorem, registered in the theorem database as field_addr_propfield_addr_prop, is

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 access composes: 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 of them — signed and unsigned, at 32 and 64 bits — over intint, taking their meaning from the machine-word semantics of HOL Light’s word library.

Every one of these is an ordinary HOL definition, not an axiom, and each definition theorem is fetchable from the theorem database under the name <op>_def<op>_def. The pattern is: wrap both operands into an N-bit word with iwordiword, apply the corresponding word operation, and read the result back as an integer — through ivalival (signed interpretation) for the i32_i32_/i64_i64_ family, and through &(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 totally. iwordiword is defined on every integer, negatives included, so u32_and (a - b) cu32_and (a - b) c is well specified even when b > ab > a. This is deliberate: unsigned C arithmetic keeps intermediates as mathematical integers in this model — there is no u32_subu32_sub — and a partial encoding would leave such terms unsimplifiable.
• Shift counts do not. The second operand of shlshl and shrshr passes through num_of_intnum_of_int, which is unspecified on negative inputs. A negative shift count is undefined behaviour in C, so nothing is lost; but a proof that must evaluate a shift has to establish that the count is non-negative.

Right shift also splits by 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 — note that the arguments come in the opposite order to the underlying cast_signedcast_signed and cast_unsignedcast_unsigned of 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 re-centres that residue into the signed window. Both are total and width-generic: they behave correctly for negative xx, and for widths of 64 bits and beyond.

Three facts about them are proved, and are available from the theorem database:

The _range_range lemmas give the result window, which is what discharges a data_atdata_at range obligation after a conversion. unsigned_last_nbits_idunsigned_last_nbits_id is the “already in range, so the conversion is the identity” law, matching exactly the condition under which the C* frontend strips 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 all the way down when it must.

C*‘s memory model folds the store into 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 those variables by a fixed naming scheme, and assertions in contracts and invariants are written using exactly these names.

The separator is a double underscore, and these are ordinary identifiers as far as the lexer is concerned: __ is an alphanumeric character in HOL Light, so x__addrx__addr is a single token, and nothing prevents a program from colliding with the convention by declaring a variable of its own by that name.

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 not a standalone pure fact in that state: it is built into the data_atdata_at resource, and is extracted with the range rule when a proof needs it.

[[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)`
int abs_diff(int a, int b);

How to write contracts and invariants over these names is developed in Function Contracts, Loop Invariants, and Assertions how they appear in the conditions the engine emits is developed in Verification Condition Generation.

• 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 lives at x + i * sizeof(ty)x + i * sizeof(ty).
• Nine ctypectype constants cover the scalar C types; sizeofsizeof, min_ofmin_of, max_ofmax_of read information out of them; 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 and width-conversion operators are defined over HOL’s machine words, not axiomatized: value operands wrap totally via iwordiword, shift counts pass through num_of_intnum_of_int (a negative count being C undefined behaviour), and the range lemmas for signed_last_nbitssigned_last_nbits and unsigned_last_nbitsunsigned_last_nbits are proved.
• Program variables reach the logic as x__addrx__addr, x__prex__pre, and __return__return.