内核头文件

C* 源文件本身就是 C 源文件。前几组页面介绍的逻辑层语法（反引号中的项、hprophprop 断言、分离逻辑连接词）都出现在 [[cst::proof]][[cst::proof]] 声明与证明块中。这些块对项或定理的一切操作，都通过调用普通的 C 函数完成。

这些函数的声明位于工具链安装的一组头文件中。cstarccstarc 会在生成的 C 文件中写入 #include <cstar.h>#include <cstar.h>，再由 cstar.hcstar.h 引入其余头文件。手写的证明代码，如 PROOFPROOF 函数、glgl 函数或操作体，编译时也使用同一套声明，因此本组页面为这两类代码提供同一套 API 参考。

下文各条目原样呈现头文件中的 C 声明及其文档注释；如果头文件还记录了相应的 HOL 命题或推理规则图，也会一并列出。

安装器将这些头文件放在 $CSTAR_HOME/include$CSTAR_HOME/include 下，默认路径为 ~/.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)

只需包含 <cstar.h><cstar.h> 即可：它会依次包含其余六个头文件，因此手写的证明文件不必逐一包含它们。这些头文件各有分工，下面分别列出它们提供的 API。

阅读后续页面时，需要注意最后一列。标为 cstarccstarc 的声明用于编译器插桩：编译器在翻译代码时，会在代码周围插入对这些函数的调用，证明代码则不会调用它们。本参考仅介绍用户会在错误消息中遇到的部分；引擎生命周期、make_*make_* 构造器与追踪记录的说明见工具链的开发者文档。

cstar.hcstar.h 自身声明了四个函数，用于向符号执行引擎注册在引擎之外定义的内容。每次验证开始时，引擎只认识一组固定的类型、谓词与策略，即内置的 C 类型、内置的谓词和已经加载的策略。规约若引用了这组内容之外的定义，就必须先注册，再让符号执行到达使用该定义的代码。

因此，应在验证正式开始之前调用这些函数，完成准备工作：用 new_datatype_definitionnew_datatype_definition 引入的类型，只有调用 cst_add_type_to_headercst_add_type_to_header 注册后才能用于规约；用 new_basic_definitionnew_basic_definition 引入的谓词，也需要先调用 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.

后两个函数与策略有关。策略是声明式的展开、折叠与消去规则，用于驱动框架推断与 PURIFY_TACPURIFY_TAC。cst_add_strategy_to_headercst_add_strategy_to_header 注册单个策略文件，并将其作为一项信任义务记入最终报告；cst_add_strategy_folder_pathcst_add_strategy_folder_path 则指定查找策略文件的目录。用策略纯化蕴含介绍了策略文件的内容，以及引擎如何使用它。

内核对象与定理介绍 proof_kernel.hproof_kernel.h：其余头文件使用的不透明句柄类型、get_T()get_T() 访问器约定、逻辑常量与分离逻辑常量的访问器，以及定理访问器目录。每个定理访问器都附有头文件中记录的 HOL 命题。如果内核中的某条定理由前面的规则推导而来，而非直接从内存模型推导得到，页面也会加以标注。

符号执行与运行时 API 介绍面向引擎的头文件，包括 symexec.hsymexec.h，以及 proof_runtime.hproof_runtime.h、proof_util.hproof_util.h 与 proof_trace.hproof_trace.h。其中，symexec.hsymexec.h 提供符号状态的读取与变换、验证条件与信任义务的报告、打印与纯化，以及错误报告等功能。

其余四页按函数操作的对象，分别介绍证明器 API hol_prover_client.hhol_prover_client.h。HOL API：类型与项介绍语法对象的构造、拆解与判定。HOL API：理论与定理介绍定义、定理数据库，以及解析与打印。HOL API：推理规则介绍 LCF 内核的十条原始规则及由它们构建的派生规则，每条都附有头文件中的推理规则图。HOL API：变换与求解器介绍各类变换、重写与判定过程。

C* 文件中的证明部分是 C 代码，调用一套有文档说明的 C API。只需包含 cstar.hcstar.h，就能使用这套 API：内核提供不透明对象与定理访问器，引擎通过符号执行产生验证条件，证明器客户端完成推理。本组页面直接从头文件生成，记录了这套 API。