内核头文件

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 的声明属于插桩：编译器会在它所翻译的代码周围生成对这些函数的调用。把它们写进文档，是为了让人能读懂生成的 C 文件及其产生的错误信息，而不是因为证明代码应该去调用它们。

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

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.

后两个函数与策略有关——策略是声明式的展开、折叠与消去规则，驱动框架推断与 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：其余各头文件所传递的不透明句柄类型、访问器约定背后的 LazyInitLazyInit 与 __DeclareTheorem__DeclareTheorem 宏、逻辑常量与分离逻辑常量的访问器，以及定理访问器的目录——每一项都配有头文件为其记录的 HOL 命题，并在内核是推导而非假设该定理之处加以标注。

符号执行与运行时 API 覆盖面向引擎的头文件：symexec.hsymexec.h——引擎生命周期、符号状态的读取与变换、验证条件与公理、纯化、错误报告，以及 cstarccstarc 生成的 make_*make_* 构造器——连同 proof_runtime.hproof_runtime.h、proof_util.hproof_util.h 与 proof_trace.hproof_trace.h。

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

C* 文件中属于证明的那一半，是面向一套有文档的 C API 编写的 C 代码。cstar.hcstar.h 是唯一需要包含的头文件；其背后是一个由不透明对象与定理访问器构成的内核、一个执行符号执行并产生验证条件的引擎，以及一个负责实施推理的证明器客户端。本组页面就是这套 API，由头文件本身生成。