Kernel Objects and Theorems

proof_kernel.hproof_kernel.h is the vocabulary of a proof block. A [[cst::proof]][[cst::proof]] function does not write separation-logic formulas as syntax; it builds them as HOL objects, and every object it needs that the logic builds in — the connectives, the heap-proposition constants, the C types, the theorems the kernel ships — reaches C code through an accessor declared in this header.

There are three kinds of thing here, and only three. Opaque handle types (termterm, thmthm, typetype, and their list and pair companions) are the currency every other header traffics in. Constant accessors — functions returning a termterm or a typetype — name the pieces of syntax a proof assembles into a goal. Theorem accessors — functions returning a thmthm — name the kernel’s proved rules, the things a proof cites. Nothing here performs inference: the rules that apply a theorem are in hol_prover_client.hhol_prover_client.h, and the engine calls that consume the result are in symexec.hsymexec.h.

This page is a name-indexed catalogue in header order. It says what is declared, under what name, and — where the header records it — the exact HOL statement the accessor returns. It does not explain the logic. The conceptual presentation, with the rules grouped by what they do, the primitive laws separated from their consequences, and the axioms flagged as axioms, is Proof Rules the predicates many of the theorems talk about are in Typed Memory Predicates.

Every logical object lives in the prover, not in the C process. The C side holds handles: pointers to structures the header declares but never defines. This is deliberate — a termterm cannot be inspected, allocated or forged by proof code, only passed back to the kernel, which is how the LCF discipline survives the language boundary (see LCF-Based Proof).

termterm is a HOL term — a formula, an expression, an hprophprop. thmthm is a theorem: a sequent the kernel has proved, and the one type C code cannot construct except through an inference rule. typetype is a HOL type, such as :hprop:hprop or :ctype:ctype. convconv is a conversion, a rewriting function from a term to an equational theorem; the conversion combinators are in HOL API: Conversions and Solvers.

The last three are results rather than syntax. instantiationinstantiation is the substitution produced by matching one term against another and consumed by the instantiation rules. indtypeindtype and inddefinddef package what new_datatype_definitionnew_datatype_definition and new_inductive_definitionnew_inductive_definition return — the induction, recursion and case theorems for a newly defined datatype or inductive relation — which is why they are structures with several theorem fields rather than single handles.

Pairs and lists are the argument types of the bulk operations. A term_pairterm_pair is one substitution component; the six list aliases rename vector types that hol_prover_client.hhol_prover_client.h declares:

These are the types that the TERM_LISTTERM_LIST and THM_LISTTHM_LIST constructors of proof_runtime.hproof_runtime.h build (see Symbolic Execution and Runtime API). Because they are typedefs rather than declarations, they are quoted verbatim here rather than listed as entries: everything below this section is generated from the header’s macro and function declarations.

Three macros stand behind every accessor on this page. They are why the catalogue is uniform: each constant and each theorem is fetched from the prover exactly once, by name, on first use.

LazyInit(type, name, f, ...)LazyInit(type, name, f, ...) defines get_<name>()get_<name>() as an inline function holding two function-local statics: a flag and the cached object. The first call evaluates f(__VA_ARGS__)f(__VA_ARGS__) — an RPC into the prover — and stores the result; every later call returns the cached handle without touching the connection. LazyInitTheorem(name)LazyInitTheorem(name) is the specialisation used for theorems: it expands to LazyInit(thm, name, get_theorem_by_name, #name)LazyInit(thm, name, get_theorem_by_name, #name), so the fetch is a lookup of the theorem’s own name in the prover’s theorem database, with #name#name stringifying the macro argument.

__DeclareTheorem(name)__DeclareTheorem(name) is the declaration counterpart. It expands to thm get_##name()thm get_##name(), so the header line

declares thm get_hsep_assoc();thm get_hsep_assoc();, and the implementation supplies the body with LazyInitTheorem(hsep_assoc)LazyInitTheorem(hsep_assoc). That is the whole convention: a theorem named TT in the kernel is reached from C as get_T()get_T(). The final line of the header does #undef __DeclareTheorem#undef __DeclareTheorem, so the macro is not visible to user code — it exists only to write the header compactly.

Four accessors return the HOL Light boolean connectives as terms. They are ordinary HOL constants, not C* additions; proof code needs them when it builds a pure side condition to hand to a decision procedure, or takes a goal of implication form apart.

These are the constants themselves, not applications: get_conj_op()get_conj_op() is the operator

/\/\

of type bool->bool->boolbool->bool->bool, to be applied with the term constructors of HOL API: Types and Terms.

The separation-logic vocabulary. get_hprop_type()get_hprop_type() returns the type :hprop:hprop of heap propositions; the rest return the constants that build one. What each means is in Memory Model and Assertions here they are the accessors, with the type each constant carries.

Two naming details are worth fixing in mind. get_hconjget_hconj returns the separating conjunction

****

, not the additive one — the additive conjunction

&&&&

is get_handget_hand. And get_hentailget_hentail and get_hequalget_hequal return

|--|--

and

-|--|-

, entailment and entailment-equivalence between heap propositions; the header’s comment for get_hequalget_hequal opens with an apostrophe instead of a backtick, which is a typo in the header and not a different constant.

The last two are not heap propositions at all: get_true_term()get_true_term() and get_false_term()get_false_term() return the boolean constants

TT

and

FF

. They appear at this point because a proof most often needs them to fill in a pure side condition — pure(T)pure(T), fact(F)fact(F) — and the header declares them here.

The logic models a C type as an element of the inductive type :ctype:ctype, and data_atdata_at, sizeofsizeof, min_ofmin_of and max_ofmax_of are all indexed by one. These accessors return that type and its nine built-in constructors, plus the two types used for struct and field names.

The TT-prefix convention is the whole naming scheme: TintTint is the logic’s name for C’s intint, TucharTuchar for unsigned charunsigned char, TptrTptr for a pointer of any pointee type. There is no accessor for TstructTstruct, the constructor taking a struct_namestruct_name: a struct type is built by applying it, and the struct’s name is a :struct_name:struct_name constant registered with cst_add_type_to_headercst_add_type_to_header (see Kernel Headers). get_struct_name_type()get_struct_name_type() and get_field_type()get_field_type() return the two types those constants inhabit; the header declares them at its very end, and they are grouped here because they belong with the C-type vocabulary rather than with the theorem catalogue. C* Extensions gives the full picture, including field_addrfield_addr and the FF-prefixed field constants.

The rest of the header is the theorem library: 141 accessors, each returning a theorem the kernel has already proved, each fetched by name from the prover’s database on first use. What follows is that catalogue, in header order.

Citing one of these is what a proof block does most: obtain the thmthm, then feed it to an inference rule from hol_prover_client.hhol_prover_client.h or to an entailment solver. What each rule is for — which are the primitive laws of the separation algebra, which are their consequences, and which are axioms the C* memory model adds — is the subject of Proof Rules and Typed Memory Predicates. The order below is the header’s, which is close to but not identical with the conceptual order those pages use.

Six general HOL Light theorems, plus the two trivial theorems about truth and falsity, are re-exported here so that proof code need not look them up by string. get_true_thm()get_true_thm() and get_false_thm()get_false_thm() are declared directly rather than through __DeclareTheorem__DeclareTheorem, which is why their entries carry the get_get_ prefix.

list_INDUCTlist_INDUCT and num_INDUCTIONnum_INDUCTION are the two induction principles a proof about a loop or a linked structure reaches for; list_CASESlist_CASES and num_CASESnum_CASES are their case-analysis counterparts. ABS_SIMPABS_SIMP is beta-reduction in equational form, and EXCLUDED_MIDDLEEXCLUDED_MIDDLE is what makes the logic classical.

The backbone. Entailment

|--|--

is reflexive and transitive, and antisymmetric with respect to

-|--|-

; the separating conjunction

****

is associative and commutative with

empemp

as unit;

-*-*

is its right adjoint; and entailment is a congruence for

****

on either side.

hsep_cancel_lefthsep_cancel_left is the frame rule of this development: from hp2 |-- hp2'hp2 |-- hp2' it concludes hp1 ** hp2 |-- hp1 ** hp2'hp1 ** hp2 |-- hp1 ** hp2', leaving hp1hp1 untouched. hsep_cancel_righthsep_cancel_right frames on the other side, and hsep_monotonehsep_monotone frames on both at once.



truetrue

and

falsefalse

as heap propositions, their relationship to purepure and factfact, their absorption behaviour under

****

, and introduction and elimination for the additive conjunction

&&&&

, disjunction

||||

and implication

-->-->

.

Note the asymmetry recorded by htrue_hemphtrue_hemp: fact(T)fact(T) is equivalent to empemp, not to truetrue. factfact carries the claim that the heap is empty; purepure does not. That distinction is the reason for two embeddings of booleans, and it is why the pure-fact rules below come in two families.

Introduction and elimination for the heap-proposition quantifiers

existsexists

and

forallforall

, which are HOL binders over a function into hprophprop.

The rules moving a pure boolean claim into and out of a heap proposition, together with the associativity and commutativity of

&&&&

that the header declares at this point.

hfact_defhfact_def fixes the relationship between the two embeddings — fact(p)fact(p) is pure(p) && emppure(p) && emp — and hfact_hpurehfact_hpure is the form used constantly in practice: fact(p) ** hpfact(p) ** hp and pure(p) && hppure(p) && hp are the same proposition. hfact_duphfact_dup is duplication, sound because a pure fact owns nothing.

How

****

and

&&&&

interact with a quantifier on the left or on the right. The existential cases are equivalences; the universal cases are entailments in one direction only, which is the expected asymmetry — a quantified separation is weaker than a separated quantification.

Congruence of entailment for the quantifiers and for the additive connectives, completing the set begun by hsep_cancel_lefthsep_cancel_left above.

Ten accessors carry a derivedderived badge, from the header’s @derived@derived marker. The marker records layering inside the kernel’s own development: these lemmas are proved from the rules above rather than belonging to the core set the separation algebra is built from. It says nothing about trust. Derived and undecorated accessors alike return theorems the prover has proved, and a proof cites them the same way.

They exist because they are the shapes that come up when an assertion is rearranged by hand: commuting a factfact past a heap proposition, pulling the second conjunct of a three-way

****

to the front, turning an equivalence into an entailment in the direction currently needed.

hsep_achsep_ac bundles the three rearrangements of a nested

****

that an associativity–commutativity normalisation needs, which is why its statement is a conjunction rather than a single equivalence.

Four accessors concern the :ctype:ctype index: the recursive equations defining sizeofsizeof, min_ofmin_of and max_ofmax_of, plus the one consequence the kernel exports directly.

A comment reading “the definition of ff” means the accessor returns the defining theorem — the conjunction of equations, one per constructor — which is what a rewriting step needs to compute sizeof Tintsizeof Tint down to a numeral. sizeof_ge_0sizeof_ge_0 is the fact that no C type has negative size, needed whenever an array address x + i * sizeof(ty)x + i * sizeof(ty) has to be bounded.

The four rules about data_atdata_at and undef_data_atundef_data_at, the memory predicates for a single typed cell, followed by the six definitional theorems for the array predicates.

data_at_rangedata_at_range is where the type index earns its keep: a stored value always lies between min_of(ty)min_of(ty) and max_of(ty)max_of(ty), and the rule makes that available as a pure fact without consuming the cell. data_at_dupdata_at_dup and undef_data_at_dupundef_data_at_dup are the anti-duplication facts that make ownership exclusive — two claims on the same address entail falsefalse.

The _def_def entries return definitions, and their comments give the signature of the predicate being defined rather than an equation. The _rec_rec variants take an explicit index range lolo, hihi; the plain array_atarray_at is the length-indexed form built on top of them; and the missing_imissing_i variants describe an array with the cell at index ii carved out, which is what a split leaves behind.

Array contents are HOL lists, so the kernel exports the list vocabulary the array rules are stated in. LENGTHLENGTH, MEMMEM, APPENDAPPEND, REVERSEREVERSE and REPLICATEREPLICATE are HOL Light’s own; the II-prefixed operations — ilengthilength, inthinth, ifirstnifirstn, iskipniskipn, ireplicateireplicate, replace_inthreplace_inth, sublistsublist — are C*‘s integer-indexed counterparts, introduced so that list indices and C’s integer arithmetic live in one type.

The last six are the proved facts about those operations that array reasoning keeps needing: that ilengthilength is non-negative and additive over append, that skipping one element off the front of a non-empty suffix behaves as expected, that skipping the whole length leaves the empty list, and the two facts about ireplicateireplicate used when an uninitialized array is filled in.

The thirty rules that make array reasoning possible: length and range facts, splitting a cell out of an array and merging it back, working at the head or the tail, rebasing an index range, dividing an array in two, and the empty case — each in an initialized array_atarray_at form and, where it makes sense, an undef_array_atundef_array_at mirror.

One addressing convention runs through all of them: element ii of an array based at xx with element type tyty lives at x + i * sizeof(ty)x + i * sizeof(ty). Typed Memory Predicates groups these same rules by what they do and works through the ones a loop invariant actually needs.

proof_kernel.hproof_kernel.h declares ten opaque handle types and six list aliases, three macros implementing the accessor convention, thirty-three accessors for the logic’s built-in terms and types, and one hundred and forty-one theorem accessors. A theorem named TT in the kernel is get_T()get_T() in C; the object is fetched from the prover once and cached for the rest of the run.

That is the entire interface between proof code and the logic’s built-in vocabulary. Everything a proof then does with the objects it obtains here — matching, instantiating, rewriting, discharging — belongs to the prover API, and everything the engine does with the results belongs to the symbolic execution API.