Kernel Headers

A C* source file is a C source file. The logic-level syntax introduced in the previous groups — terms in backticks, hprophprop assertions, and separation-logic connectives — appears inside [[cst::proof]][[cst::proof]] declarations and proof blocks. Every operation on a term or theorem in these blocks calls an ordinary C function.

These functions are declared in a small set of headers installed by the toolchain. cstarccstarc writes #include <cstar.h>#include <cstar.h> into the C file it emits, and cstar.hcstar.h includes the remaining headers. Hand-written proof code — a PROOFPROOF function, a glgl function, or an operation body — compiles against the same declarations, so this group provides the API reference for both generated and hand-written code.

Each entry below reproduces the C declaration and its documentation comment from the header, along with the corresponding HOL statement or inference-rule diagram where one is provided.

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 sufficient: it includes the other six headers, so a hand-written proof file does not need to include them individually. The table below lists the API provided by each header.

The last column distinguishes the callers of each API. Entries marked for both user and cstarccstarc calls are shared APIs. The compiler-only entries provide instrumentation: the compiler emits calls to them around the code it translates, and proof code does not call them. This reference documents compiler-only instrumentation only where it appears in user-facing error messages. The engine lifecycle, the make_*make_* builders, and trace bookkeeping are described in the toolchain’s developer documentation.

cstar.hcstar.h declares four functions for registering externally defined objects with the symbolic execution engine. A verification run starts with a fixed vocabulary: the built-in C types, the built-in predicates, and the strategies already loaded. Any definition a specification uses beyond this vocabulary must be registered before symbolic execution reaches the code that uses it.

Call these functions during setup, before verification begins: a type introduced with new_datatype_definitionnew_datatype_definition becomes usable in specifications only after registration with cst_add_type_to_headercst_add_type_to_header, and a predicate introduced with new_basic_definitionnew_basic_definition only after registration with 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 functions 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 specifies a directory to search for these files. Purifying Entailments with Strategies describes the contents of a strategy file and how the engine uses it.

Kernel Objects and Theorems covers proof_kernel.hproof_kernel.h: the opaque handle types used by every other header, the get_T()get_T() accessor convention, the accessors for logical and separation-logic constants, and the catalogue of theorem accessors. Each theorem accessor is paired with the HOL statement recorded in the header. The page also indicates which theorems the kernel derives from preceding rules rather than directly from the memory model.

Symbolic Execution and Runtime API covers the engine-facing headers. It describes symexec.hsymexec.h for reading and transforming the symbolic state, reporting verification conditions and trust obligations, printing and purification, and error reporting. It also covers 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, grouped by the objects 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 decision procedures.

The proof portion of a C* file is C code that calls a documented C API. Including cstar.hcstar.h gives access to the kernel’s opaque objects and theorem accessors, the engine that performs symbolic execution and produces verification conditions, and the prover client that carries out inference. This group documents the API directly from its headers.