Kernel Headers

A C* source file is a C source file. The logic-level syntax of the previous groups — terms in backticks, hprophprop assertions, the separation-logic connectives — lives inside [[cst::proof]][[cst::proof]] declarations and proof blocks, and everything those blocks do with a term or a theorem, they do by calling an ordinary C function.

Those functions are declared in a small family of headers that the toolchain installs. cstarccstarc writes #include <cstar.h>#include <cstar.h> into the C file it emits, and cstar.hcstar.h pulls in the rest of the family. Proof code written by hand — a PROOFPROOF function, a glgl function, an operation body — compiles against exactly the same declarations, so this group is the API reference for both.

Each entry below appears as the header declares it: the C declaration, the doc comment shipped with it, and, where the header carries one, the HOL statement or inference-rule diagram it stands for.

The installer places the headers under $CSTAR_HOME/include$CSTAR_HOME/include, which defaults to ~/.cstar/include~/.cstar/include:

~/.cstar/include/
├── cstar.h                 # the umbrella header cstarc includes
├── proof_kernel.h          # opaque types, term/type constants, theorem accessors
├── proof_runtime.h         # argument-list constructors for emitted code
├── proof_trace.h           # proof-side stack trace for runtime failures
├── proof_util.h            # error-handling macros and string helpers
├── symexec.h               # symbolic execution engine + AST builders
├── hol_prover_client.h     # the HOL Light prover API
└── gc/  log/  vec/         # third-party support libraries (not documented here)

~/.cstar/include/
├── cstar.h                 # the umbrella header cstarc includes
├── proof_kernel.h          # opaque types, term/type constants, theorem accessors
├── proof_runtime.h         # argument-list constructors for emitted code
├── proof_trace.h           # proof-side stack trace for runtime failures
├── proof_util.h            # error-handling macros and string helpers
├── symexec.h               # symbolic execution engine + AST builders
├── hol_prover_client.h     # the HOL Light prover API
└── gc/  log/  vec/         # third-party support libraries (not documented here)

Including <cstar.h><cstar.h> is enough: it includes the other six in turn, so a hand-written proof file never needs to name them individually. They are listed separately here because they divide the API along useful lines.

The last column matters when reading the pages that follow. Declarations marked cstarccstarc are compiler instrumentation: the compiler emits calls to them around the code it translates, and proof code never calls them. They are not documented in this reference beyond what a user meets in an error message; the engine lifecycle, the make_*make_* builders and the trace bookkeeping are described in the toolchain’s own developer documentation.

cstar.hcstar.h declares four functions of its own, and they all do the same kind of thing: they tell the symbolic execution engine about something defined outside it. A verification run starts from a fixed vocabulary — the built-in C types, the built-in predicates, the strategies already loaded. Anything a specification mentions beyond that must be registered before symbolic execution reaches the code that uses it.

Calls to these functions therefore belong to the setup that runs before verification proper: a type introduced with new_datatype_definitionnew_datatype_definition becomes usable in specifications only after cst_add_type_to_headercst_add_type_to_header, and a predicate introduced with new_basic_definitionnew_basic_definition only after cst_add_const_to_headercst_add_const_to_header.

int cst_add_type_to_header(const char* name, int arity);

int cst_add_type_to_header(const char* name, int arity);

Notes the symbolic execution engine for an external type.

• name — The name of the type.
• arity — The number of type arguments.
• returns — zero if succceeded, otherwise returns non-zero.
• raises — Sets error status if failed.

int cst_add_const_to_header(term tm);

int cst_add_const_to_header(term tm);

Notes the symbolic execution engine for an external constant or function.

• tm — The constant to be exported.
• returns — zero if succceeded, otherwise returns non-zero.
• raises — Sets error status if failed.

int cst_add_strategy_to_header(const char* filename);

int cst_add_strategy_to_header(const char* filename);

Loads a strategy file and records it as a trust obligation in the final report. Repeated calls are recorded in order.

• filename — The path to the file.
• returns — zero on success, otherwise non-zero.

int cst_add_strategy_folder_path(const char* path);

int cst_add_strategy_folder_path(const char* path);

Adds a path as strategy folder for the symbolic execution engine.

• path — The path.
• raises — Fails if the path is invalid.

The last two concern strategies — the declarative unfold, fold and cancel rules that drive frame inference and PURIFY_TACPURIFY_TAC. cst_add_strategy_to_headercst_add_strategy_to_header registers a single strategy file and records it as a trust obligation in the final report, cst_add_strategy_folder_pathcst_add_strategy_folder_path names a directory to look for such files in; Purifying Entailments with Strategies describes what goes inside such a file and how the engine uses it.

Kernel Objects and Theorems covers proof_kernel.hproof_kernel.h: the opaque handle types every other header traffics in, the get_T()get_T() accessor convention, the accessors for the logical and separation-logic constants, and the catalogue of theorem accessors — each paired with the HOL statement the header records for it, and marked where the kernel derives it from the rules before it rather than directly from the memory model.

Symbolic Execution and Runtime API covers the engine-facing headers: symexec.hsymexec.h — reading and transforming the symbolic state, the report of verification conditions and trust obligations, printing and purification, and how errors are reported — together with proof_runtime.hproof_runtime.h, proof_util.hproof_util.h and proof_trace.hproof_trace.h.

The remaining four pages cover hol_prover_client.hhol_prover_client.h, the prover API, split by what the functions operate on. HOL API: Types and Terms covers the construction, destruction and testing of syntactic objects. HOL API: Theories and Theorems covers definitions, the theorem database, and parsing and printing. HOL API: Inference Rules covers the ten primitive rules of the LCF kernel and the derived rules built on them, each with the inference-rule diagram from the header. HOL API: Conversions and Solvers covers conversions, rewriting and the decision procedures.

The proof half of a C* file is C code against a documented C API. cstar.hcstar.h is the single include; behind it sit a kernel of opaque objects and theorem accessors, an engine that performs symbolic execution and produces verification conditions, and a prover client that carries out the inference. This group is that API, generated from the headers themselves.