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 instrumentation: the compiler emits calls to them around the code it translates. They are documented so that a generated C file and the error messages it produces can be read — not because proof code should call them.

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);

For strategy. Notes the engine a file for strategies.

• filename — The path to the file.
• returns — 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, cst_add_strategy_folder_pathcst_add_strategy_folder_path a whole directory of them; 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 LazyInitLazyInit and __DeclareTheorem__DeclareTheorem macros behind the 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 rather than assumes it.

Symbolic Execution and Runtime API covers the engine-facing headers: symexec.hsymexec.h — engine lifecycle, reading and transforming the symbolic state, verification conditions and axioms, purification, error reporting, and the make_*make_* builders cstarccstarc emits — 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, parsing and printing, and session checkpoints. 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.