内核对象与定理

EN | 中文

内核对象与定理

proof_kernel.hproof_kernel.h 提供了证明块所用的基本词汇。在 [[cst::proof]][[cst::proof]] 函数中，分离逻辑公式需要构造为 HOL 对象，不能直接按公式语法书写。证明所需的逻辑内置对象，包括连接词、堆命题常量、C 类型和内核自带的定理，都通过这个头文件声明的访问器供 C 代码使用。

这里的接口只有三类。不透明句柄类型（termterm、thmthm、typetype，以及配套的列表与配对类型）供其他头文件共同使用。常量访问器返回 termterm 或 typetype，按名称提供构造待证目标所需的语法片段。定理访问器返回 thmthm，按名称提供内核已经证明的规则，供证明引用。这些接口本身不执行推理：应用定理的规则在 hol_prover_client.hhol_prover_client.h 中，使用推理结果的引擎调用在 symexec.hsymexec.h 中。

本页按头文件中的顺序列出各项声明，供读者按名称查阅。若头文件有所记录，还会给出访问器返回的确切 HOL 陈述。逻辑本身的概念讲解见证明规则页，其中按作用对规则分组，并区分基本定律及其推论；许多定理所涉及的谓词见带类型的内存谓词页。

如何阅读一个条目

每个条目先原样给出头文件中的 C 声明，随后列出头文件注释所记录的 HOL 陈述：可能是定理的陈述、常量的类型，也可能是一条注记，说明该访问器返回某个定义。种类徽标把 theoremtheorem 与 term-constterm-const、typetype、macromacro 区分开来，第二个 derivedderived 徽标则标出头文件标注了 @derived@derived 的条目。右侧的灰色标记给出该条目在仓库内置头文件副本中的源码位置，便于对照来源文件核查。

每个条目还有一个以条目名称命名的锚点：hsep_assochsep_assoc 的访问器位于本页的 #api-hsep_assoc#api-hsep_assoc 片段处，因此可以按名称链接到某一条规则。

不透明类型

逻辑对象都保存在证明器中，不在 C 进程中。C 侧持有的句柄是指向结构体的指针，而头文件只声明这些结构体，从不定义它们。这一设计使证明代码无法检查、分配或伪造 termterm，只能将句柄传回内核，因此即使跨越语言边界，仍能遵守 LCF 规范（见基于 LCF 架构的证明）。


typedef struct hol_term term;
typedef struct hol_theorem thm;
typedef struct hol_type type;
typedef struct hol_conversion conv;
typedef struct hol_term_pair term_pair;
typedef struct hol_thm_pair thm_pair;
typedef struct hol_type_pair type_pair;
typedef struct hol_instantiation instantiation;
typedef struct new_datatype_definition_results indtype;
typedef struct new_inductive_definition_results inddef;


typedef struct hol_term term;
typedef struct hol_theorem thm;
typedef struct hol_type type;
typedef struct hol_conversion conv;
typedef struct hol_term_pair term_pair;
typedef struct hol_thm_pair thm_pair;
typedef struct hol_type_pair type_pair;
typedef struct hol_instantiation instantiation;
typedef struct new_datatype_definition_results indtype;
typedef struct new_inductive_definition_results inddef;

termterm 是 HOL 项，可以是公式、表达式或 hprophprop。thmthm 是定理：内核已经证明的相继式，也是唯一一种 C 代码必须通过推理规则才能构造的类型。typetype 是 HOL 类型，如 :hprop:hprop 或 :ctype:ctype。convconv 是变换，即把项映射到等式定理的重写函数；变换组合子见 HOL API：变换与求解器页。

最后三个类型表示操作结果，而非语法。instantiationinstantiation 表示将一个项与另一个项匹配后得到的替换，供实例化规则使用。indtypeindtype 与 inddefinddef 封装 new_datatype_definitionnew_datatype_definition 和 new_inductive_definitionnew_inductive_definition 的返回结果，即新定义的数据类型或归纳关系所对应的归纳定理、递归定理与分情况定理。因此它们是带若干定理字段的结构体，而不是单个句柄。

配对与列表是批量操作的参数类型。term_pairterm_pair 表示替换的一个分量；六个列表别名对应 hol_prover_client.hhol_prover_client.h 声明的向量类型：


typedef hol_term_list term_list;
typedef hol_theorem_list thm_list;
typedef hol_type_list type_list;
typedef hol_term_pair_list term_pair_list;
typedef hol_thm_pair_list thm_pair_list;
typedef hol_type_pair_list type_pair_list;


typedef hol_term_list term_list;
typedef hol_theorem_list thm_list;
typedef hol_type_list type_list;
typedef hol_term_pair_list term_pair_list;
typedef hol_thm_pair_list thm_pair_list;
typedef hol_type_pair_list type_pair_list;

proof_runtime.hproof_runtime.h 的 TERM_LISTTERM_LIST 与 THM_LISTTHM_LIST 构造子所生成的正是这些类型（见符号执行与运行时 API页）。由于它们是 typedef，而非声明，这里直接原样引用，不单列条目：本节以下的全部内容都由头文件中的宏声明与函数声明生成。

访问器宏

本页的访问器都遵循同一约定：内核中名为 TT 的常量或定理，在 C 侧通过 get_T()get_T() 获取。对象在首次使用时按名称从证明器取回，随后缓存到本次运行结束。头文件用三个宏实现这一约定，其中最后一个 __DeclareTheorem__DeclareTheorem 用来声明下文的定理访问器。这些宏用于实现头文件自身的机制，并非供证明代码使用的 API，因此这里只列出名称，不作详细说明：

LazyInitLazyInit, LazyInitTheoremLazyInitTheorem, __DeclareTheorem__DeclareTheorem — 访问器约定的实现；证明代码调用的是 get_*get_* 函数，从不调用这些宏。

逻辑连接词

四个访问器以项的形式返回 HOL Light 的布尔连接词。它们是普通的 HOL 常量，并非 C* 新增的常量；证明代码在构造交给判定过程的纯附加条件，或者拆解蕴含形式的待证目标时会用到它们。

get_conj_opterm-constproof_kernel.h:44


term get_conj_op();


term get_conj_op();


/\ : bool->bool->bool


/\ : bool->bool->bool

get_disj_opterm-constproof_kernel.h:47


term get_disj_op();


term get_disj_op();


\/ : bool->bool->bool


\/ : bool->bool->bool

get_iff_opterm-constproof_kernel.h:50


term get_iff_op();


term get_iff_op();


<=> : bool->bool->bool


<=> : bool->bool->bool

get_imp_opterm-constproof_kernel.h:53


term get_imp_op();


term get_imp_op();


==> : bool->bool->bool


==> : bool->bool->bool

返回的是常量本身，而不是应用式：get_conj_op()get_conj_op() 是类型为 bool->bool->boolbool->bool->bool 的运算符 /\/\ ，需要用 HOL API：类型与项页中的项构造子将它应用到参数上。

堆命题常量

这些常量构成分离逻辑的基本词汇。get_hprop_type()get_hprop_type() 返回堆命题的类型 :hprop:hprop；其余访问器返回构造堆命题的各个常量。每个常量的含义见内存模型与断言页；这里给出的是访问器，以及每个常量的类型。

get_hprop_typetypeproof_kernel.h:56


type get_hprop_type();


type get_hprop_type();


:hprop


:hprop

get_hfactterm-constproof_kernel.h:59


term get_hfact();


term get_hfact();


fact : bool->hprop


fact : bool->hprop

get_hentailterm-constproof_kernel.h:62


term get_hentail();


term get_hentail();


|-- : hprop->hprop->hprop


|-- : hprop->hprop->hprop

get_hequalterm-constproof_kernel.h:65


term get_hequal();


term get_hequal();


-|- : hprop->hprop->hprop


-|- : hprop->hprop->hprop

get_hconjterm-constproof_kernel.h:68


term get_hconj();


term get_hconj();


** : hprop->hprop->hprop


** : hprop->hprop->hprop

get_hempterm-constproof_kernel.h:71


term get_hemp();


term get_hemp();


emp : hprop


emp : hprop

get_htrueterm-constproof_kernel.h:74


term get_htrue();


term get_htrue();


true : hprop


true : hprop

get_hfalseterm-constproof_kernel.h:77


term get_hfalse();


term get_hfalse();


false : hprop


false : hprop

get_hwandterm-constproof_kernel.h:80


term get_hwand();


term get_hwand();


-* : hprop->hprop->hprop


-* : hprop->hprop->hprop

get_himplterm-constproof_kernel.h:83


term get_himpl();


term get_himpl();


--> : hprop->hprop->hprop


--> : hprop->hprop->hprop

get_horterm-constproof_kernel.h:86


term get_hor();


term get_hor();


|| : hprop->hprop->hprop


|| : hprop->hprop->hprop

get_handterm-constproof_kernel.h:89


term get_hand();


term get_hand();


&& : hprop->hprop->hprop


&& : hprop->hprop->hprop

get_hforallterm-constproof_kernel.h:92


term get_hforall();


term get_hforall();


forall : (A->hprop)->hprop


forall : (A->hprop)->hprop

get_hexiststerm-constproof_kernel.h:95


term get_hexists();


term get_hexists();


exists : (A->hprop)->hprop


exists : (A->hprop)->hprop

get_hpureterm-constproof_kernel.h:98


term get_hpure();


term get_hpure();


pure : bool->hprop


pure : bool->hprop

get_true_termterm-constproof_kernel.h:101


term get_true_term();


term get_true_term();


T : bool


T : bool

get_false_termterm-constproof_kernel.h:104


term get_false_term();


term get_false_term();


F : bool


F : bool

有两点命名细节需要注意。get_hconjget_hconj 返回的是分离合取 **** ，而不是加性合取；加性合取 &&&& 对应的是 get_handget_hand。另外，get_hentailget_hentail 与 get_hequalget_hequal 返回 |--|-- 和 -|--|- ，即堆命题之间的蕴含与蕴含等价。

最后两个访问器返回的并非堆命题：get_true_term()get_true_term() 与 get_false_term()get_false_term() 返回布尔常量 TT 和 FF 。它们出现在这里，是因为证明最常用它们来构造纯附加条件，如 pure(T)pure(T)、fact(F)fact(F)，而头文件也正是在此处声明它们的。

C 类型、结构体与字段

逻辑将每个 C 类型建模为归纳类型 :ctype:ctype 的一个元素，而 data_atdata_at、sizeofsizeof、min_ofmin_of 与 max_ofmax_of 都以它为索引。这些访问器返回该类型及其九个内置构造子，另加用于结构体名与字段名的两个类型。

get_ctype_typetypeproof_kernel.h:343


type get_ctype_type();


type get_ctype_type();


:ctype


:ctype

get_Tcharterm-constproof_kernel.h:346


term get_Tchar();


term get_Tchar();


Tchar : ctype


Tchar : ctype

get_Tucharterm-constproof_kernel.h:349


term get_Tuchar();


term get_Tuchar();


Tuchar : ctype


Tuchar : ctype

get_Tshortterm-constproof_kernel.h:352


term get_Tshort();


term get_Tshort();


Tshort : ctype


Tshort : ctype

get_Tushortterm-constproof_kernel.h:355


term get_Tushort();


term get_Tushort();


Tushort : ctype


Tushort : ctype

get_Tintterm-constproof_kernel.h:358


term get_Tint();


term get_Tint();


Tint : ctype


Tint : ctype

get_Tuintterm-constproof_kernel.h:361


term get_Tuint();


term get_Tuint();


Tuint : ctype


Tuint : ctype

get_Tint64term-constproof_kernel.h:364


term get_Tint64();


term get_Tint64();


Tint64 : ctype


Tint64 : ctype

get_Tuint64term-constproof_kernel.h:367


term get_Tuint64();


term get_Tuint64();


Tuint64 : ctype


Tuint64 : ctype

get_Tptrterm-constproof_kernel.h:370


term get_Tptr();


term get_Tptr();


Tptr : ctype


Tptr : ctype

get_struct_name_typetypeproof_kernel.h:631


type get_struct_name_type();


type get_struct_name_type();


:struct_name


:struct_name

get_field_typetypeproof_kernel.h:634


type get_field_type();


type get_field_type();


:field


:field

这些名称统一采用 TT 前缀：TintTint 在逻辑中表示 C 的 intint，TucharTuchar 对应 unsigned charunsigned char，TptrTptr 对应指针，其所指对象可以是任意类型。接受 struct_namestruct_name 的构造子 TstructTstruct 没有访问器：要构造结构体类型，需要将它应用到结构体名称上；结构体名称则是用 cst_add_type_to_headercst_add_type_to_header 注册的 :struct_name:struct_name 常量（见内核头文件页）。get_struct_name_type()get_struct_name_type() 与 get_field_type()get_field_type() 返回这些常量所属的两个类型；头文件把它们声明在最末尾，这里之所以把它们归入本节，是因为它们属于 C 类型词汇，而不属于定理目录。 C* 的扩展页作了完整介绍，包括 field_addrfield_addr 与以 FF 为前缀的字段常量。

定理访问器

头文件的其余部分是定理库，共有 160 个访问器。每个访问器返回一条内核已经证明的定理，在首次使用时按名称从证明器的数据库中取回。以下按头文件顺序列出这些访问器。

证明块最常做的操作就是引用其中的定理：取得 thmthm，再把它传给 hol_prover_client.hhol_prover_client.h 中的推理规则或蕴含求解器。每条规则用来做什么，是证明规则页与带类型的内存谓词页的主题。下面采用的是头文件的顺序，它与那两页所用的概念顺序接近，但并不相同。

HOL 基础

六条通用的 HOL Light 定理，加上关于真与假的两条平凡定理，在这里重新导出，这样证明代码就不必用字符串去查找它们。get_true_thm()get_true_thm() 与 get_false_thm()get_false_thm() 是直接声明的，没有经过 __DeclareTheorem__DeclareTheorem，因此它们的条目名带有 get_get_ 前缀。

get_true_thmtheoremproof_kernel.h:107


thm get_true_thm();


thm get_true_thm();


|- T


|- T

get_false_thmtheoremproof_kernel.h:110


thm get_false_thm();


thm get_false_thm();


|- !t. F ==> t


|- !t. F ==> t

ABS_SIMPtheoremproof_kernel.h:113


thm get_ABS_SIMP();


thm get_ABS_SIMP();


!t1 t2. (\x. t1) t2 = t1


!t1 t2. (\x. t1) t2 = t1

EXCLUDED_MIDDLEtheoremproof_kernel.h:116


thm get_EXCLUDED_MIDDLE();


thm get_EXCLUDED_MIDDLE();


!t. t \/ ~t


!t. t \/ ~t

list_CASEStheoremproof_kernel.h:119


thm get_list_CASES();


thm get_list_CASES();


!l. l = [] \/ (?h t. l = CONS h t)


!l. l = [] \/ (?h t. l = CONS h t)

list_INDUCTtheoremproof_kernel.h:122


thm get_list_INDUCT();


thm get_list_INDUCT();


!P. P [] /\ (!a0 a1. P a1 ==> P (CONS a0 a1)) ==> (!x. P x)


!P. P [] /\ (!a0 a1. P a1 ==> P (CONS a0 a1)) ==> (!x. P x)

num_CASEStheoremproof_kernel.h:125


thm get_num_CASES();


thm get_num_CASES();


!m. m = 0 \/ (?n. m = SUC n)


!m. m = 0 \/ (?n. m = SUC n)

num_INDUCTIONtheoremproof_kernel.h:128


thm get_num_INDUCTION();


thm get_num_INDUCTION();


!P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)


!P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)

list_INDUCTlist_INDUCT 与 num_INDUCTIONnum_INDUCTION 是两条归纳原理，用于证明循环或链式结构的性质； list_CASESlist_CASES 与 num_CASESnum_CASES 是与之对应的分情况分析定理。ABS_SIMPABS_SIMP 是等式形式的 beta 归约，EXCLUDED_MIDDLEEXCLUDED_MIDDLE 则使这套逻辑成为经典逻辑。

蕴含与分离合取

这一组是基本规则。蕴含 |--|-- 具有自反性与传递性，并在 -|--|- 意义下具有反对称性；分离合取 **** 满足结合律与交换律，以 empemp 为单位元； -*-* 是它的右伴随；而蕴含对 **** 的任一侧都构成合同关系。

hentail_refltheoremproof_kernel.h:131


thm get_hentail_refl();


thm get_hentail_refl();


!hp. hp |-- hp


!hp. hp |-- hp

hentail_transtheoremproof_kernel.h:134


thm get_hentail_trans();


thm get_hentail_trans();


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp2 |-- hp3) ==> (hp1 |-- hp3)


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp2 |-- hp3) ==> (hp1 |-- hp3)

hentail_antisymtheoremproof_kernel.h:137


thm get_hentail_antisym();


thm get_hentail_antisym();


!hp1 hp2. (hp1 |-- hp2) ==> (hp2 |-- hp1) ==> (hp1 -|- hp2)


!hp1 hp2. (hp1 |-- hp2) ==> (hp2 |-- hp1) ==> (hp1 -|- hp2)

hsep_assoctheoremproof_kernel.h:140


thm get_hsep_assoc();


thm get_hsep_assoc();


!hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)


!hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)

hsep_commtheoremproof_kernel.h:143


thm get_hsep_comm();


thm get_hsep_comm();


!hp1 hp2. hp1 ** hp2 -|- hp2 ** hp1


!hp1 hp2. hp1 ** hp2 -|- hp2 ** hp1

hsep_hemp_lefttheoremproof_kernel.h:146


thm get_hsep_hemp_left();


thm get_hsep_hemp_left();


!hp. emp ** hp -|- hp


!hp. emp ** hp -|- hp

hsep_hemp_righttheoremproof_kernel.h:149


thm get_hsep_hemp_right();


thm get_hsep_hemp_right();


!hp. hp ** emp -|- hp


!hp. hp ** emp -|- hp

hwand_hsep_adjointtheoremproof_kernel.h:152


thm get_hwand_hsep_adjoint();


thm get_hwand_hsep_adjoint();


!hp1 hp2 hp3. (hp1 ** hp2 |-- hp3) <=> (hp1 |-- hp2 -* hp3)


!hp1 hp2 hp3. (hp1 ** hp2 |-- hp3) <=> (hp1 |-- hp2 -* hp3)

hsep_cancel_lefttheoremproof_kernel.h:155


thm get_hsep_cancel_left();


thm get_hsep_cancel_left();


!hp2 hp2' hp1. (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1 ** hp2')


!hp2 hp2' hp1. (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1 ** hp2')

hsep_cancel_righttheoremproof_kernel.h:158


thm get_hsep_cancel_right();


thm get_hsep_cancel_right();


!hp1 hp1' hp2. (hp1 |-- hp1') ==> (hp1 ** hp2 |-- hp1' ** hp2)


!hp1 hp1' hp2. (hp1 |-- hp1') ==> (hp1 ** hp2 |-- hp1' ** hp2)

hsep_monotonetheoremproof_kernel.h:161


thm get_hsep_monotone();


thm get_hsep_monotone();


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')

hsep_cancel_lefthsep_cancel_left 是这套理论中的框架规则：由 hp2 |-- hp2'hp2 |-- hp2' 得出 hp1 ** hp2 |-- hp1 ** hp2'hp1 ** hp2 |-- hp1 ** hp2'，hp1hp1 保持不变。hsep_cancel_righthsep_cancel_right 在另一侧应用框架规则， hsep_monotonehsep_monotone 则同时作用于两侧。

真、假与加性连接词

作为堆命题的 truetrue 与 falsefalse 、它们与 purepure 和 factfact 的关系、它们在 **** 下的吸收性质，以及加性合取 &&&& 、析取 |||| 与蕴含 -->--> 的引入与消去规则。

htrue_deftheoremproof_kernel.h:164


thm get_htrue_def();


thm get_htrue_def();


true -|- pure(T)


true -|- pure(T)

hfalse_deftheoremproof_kernel.h:167


thm get_hfalse_def();


thm get_hfalse_def();


false -|- pure(F)


false -|- pure(F)

htrue_introtheoremproof_kernel.h:170


thm get_htrue_intro();


thm get_htrue_intro();


!hp. hp |-- true


!hp. hp |-- true

htrue_hemptheoremproof_kernel.h:173


thm get_htrue_hemp();


thm get_htrue_hemp();


fact(T) -|- emp


fact(T) -|- emp

hfalse_elimtheoremproof_kernel.h:176


thm get_hfalse_elim();


thm get_hfalse_elim();


!hp. false |-- hp


!hp. false |-- hp

hfact_false_elimtheoremproof_kernel.h:179


thm get_hfact_false_elim();


thm get_hfact_false_elim();


!hp. fact(F) |-- hp


!hp. fact(F) |-- hp

htrue_elim_lefttheoremproof_kernel.h:182


thm get_htrue_elim_left();


thm get_htrue_elim_left();


!hp. fact(T) ** hp -|- hp


!hp. fact(T) ** hp -|- hp

htrue_elim_righttheoremproof_kernel.h:185


thm get_htrue_elim_right();


thm get_htrue_elim_right();


!hp. hp ** fact(T) -|- hp


!hp. hp ** fact(T) -|- hp

hfalse_absorb_lefttheoremproof_kernel.h:188


thm get_hfalse_absorb_left();


thm get_hfalse_absorb_left();


!hp. fact(F) ** hp -|- fact(F)


!hp. fact(F) ** hp -|- fact(F)

hfalse_absorb_righttheoremproof_kernel.h:191


thm get_hfalse_absorb_right();


thm get_hfalse_absorb_right();


!hp. hp ** fact(F) -|- fact(F)


!hp. hp ** fact(F) -|- fact(F)

hand_introtheoremproof_kernel.h:194


thm get_hand_intro();


thm get_hand_intro();


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 |-- hp3) ==> (hp1 |-- hp2 && hp3)


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 |-- hp3) ==> (hp1 |-- hp2 && hp3)

hand_elim1theoremproof_kernel.h:197


thm get_hand_elim1();


thm get_hand_elim1();


!hp1 hp2. (hp1 && hp2 |-- hp1)


!hp1 hp2. (hp1 && hp2 |-- hp1)

hand_elim2theoremproof_kernel.h:200


thm get_hand_elim2();


thm get_hand_elim2();


!hp1 hp2. (hp1 && hp2 |-- hp2)


!hp1 hp2. (hp1 && hp2 |-- hp2)

hor_intro1theoremproof_kernel.h:203


thm get_hor_intro1();


thm get_hor_intro1();


!hp1 hp2. (hp1 |-- hp1 || hp2)


!hp1 hp2. (hp1 |-- hp1 || hp2)

hor_intro2theoremproof_kernel.h:206


thm get_hor_intro2();


thm get_hor_intro2();


!hp1 hp2. (hp2 |-- hp1 || hp2)


!hp1 hp2. (hp2 |-- hp1 || hp2)

hor_elimtheoremproof_kernel.h:209


thm get_hor_elim();


thm get_hor_elim();


!hp1 hp2 hp3. (hp1 |-- hp3) ==> (hp2 |-- hp3) ==> (hp1 || hp2 |-- hp3)


!hp1 hp2 hp3. (hp1 |-- hp3) ==> (hp2 |-- hp3) ==> (hp1 || hp2 |-- hp3)

himpl_hand_adjointtheoremproof_kernel.h:212


thm get_himpl_hand_adjoint();


thm get_himpl_hand_adjoint();


!hp1 hp2 hp3. (hp1 && hp2 |-- hp3) <=> (hp1 |-- hp2 --> hp3)


!hp1 hp2 hp3. (hp1 && hp2 |-- hp3) <=> (hp1 |-- hp2 --> hp3)

注意 htrue_hemphtrue_hemp 所记录的不对称：fact(T)fact(T) 等价于 empemp，而不等价于 truetrue。factfact 携带“堆为空”这一断言，purepure 则不携带。这一区别正是布尔值需要两种嵌入的原因，也是下面的纯事实规则分成两族的原因。

量词规则

堆命题量词 existsexists 与 forallforall 的引入与消去规则；它们是作用于返回 hprophprop 的函数的 HOL 绑定子。

hexists_introtheoremproof_kernel.h:215


thm get_hexists_intro();


thm get_hexists_intro();


!(x : A) hp hpA. (hp |-- hpA x) ==> (hp |-- (exists x : A. hpA x))


!(x : A) hp hpA. (hp |-- hpA x) ==> (hp |-- (exists x : A. hpA x))

hexists_elimtheoremproof_kernel.h:218


thm get_hexists_elim();


thm get_hexists_elim();


!hp hpA. (!x : A. hpA x |-- hp) ==> ((exists y : A. hpA y) |-- hp)


!hp hpA. (!x : A. hpA x |-- hp) ==> ((exists y : A. hpA y) |-- hp)

hforall_introtheoremproof_kernel.h:221


thm get_hforall_intro();


thm get_hforall_intro();


!hp hpA. (!x : A. hp |-- hpA x) ==> (hp |-- (forall x : A. hpA x))


!hp hpA. (!x : A. hp |-- hpA x) ==> (hp |-- (forall x : A. hpA x))

hforall_elimtheoremproof_kernel.h:224


thm get_hforall_elim();


thm get_hforall_elim();


!hp hpA (x : A). (hpA x |-- hp) ==> ((forall x : A. hpA x) |-- hp)


!hp hpA (x : A). (hpA x |-- hp) ==> ((forall x : A. hpA x) |-- hp)

纯事实

把纯布尔断言移入、移出堆命题的规则，以及头文件在此处声明的 &&&& 的结合律与交换律。

hpure_introtheoremproof_kernel.h:227


thm get_hpure_intro();


thm get_hpure_intro();


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- pure(p) && hp2)


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- pure(p) && hp2)

hpure_elimtheoremproof_kernel.h:230


thm get_hpure_elim();


thm get_hpure_elim();


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (pure(p) && hp1 |-- hp2)


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (pure(p) && hp1 |-- hp2)

hand_assoctheoremproof_kernel.h:233


thm get_hand_assoc();


thm get_hand_assoc();


!hp1 hp2 hp3. (hp1 && hp2) && hp3 -|- hp1 && (hp2 && hp3)


!hp1 hp2 hp3. (hp1 && hp2) && hp3 -|- hp1 && (hp2 && hp3)

hand_commtheoremproof_kernel.h:236


thm get_hand_comm();


thm get_hand_comm();


!hp1 hp2. hp1 && hp2 -|- hp2 && hp1


!hp1 hp2. hp1 && hp2 -|- hp2 && hp1

hsep_hpure_lefttheoremproof_kernel.h:239


thm get_hsep_hpure_left();


thm get_hsep_hpure_left();


!p hp1 hp2. (pure(p) && hp1) ** hp2 -|- pure(p) && (hp1 ** hp2)


!p hp1 hp2. (pure(p) && hp1) ** hp2 -|- pure(p) && (hp1 ** hp2)

hsep_hpure_righttheoremproof_kernel.h:242


thm get_hsep_hpure_right();


thm get_hsep_hpure_right();


!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)


!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)

hfact_deftheoremproof_kernel.h:245


thm get_hfact_def();


thm get_hfact_def();


!p hp. fact(p) -|- (pure(p) && emp)


!p hp. fact(p) -|- (pure(p) && emp)

hfact_hpuretheoremproof_kernel.h:248


thm get_hfact_hpure();


thm get_hfact_hpure();


!p hp. fact(p) ** hp -|- pure(p) && hp


!p hp. fact(p) ** hp -|- pure(p) && hp

hfact_introtheoremproof_kernel.h:251


thm get_hfact_intro();


thm get_hfact_intro();


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- fact(p) ** hp2)


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- fact(p) ** hp2)

hfact_elimtheoremproof_kernel.h:254


thm get_hfact_elim();


thm get_hfact_elim();


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- hp2)


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- hp2)

hfact_duptheoremproof_kernel.h:257


thm get_hfact_dup();


thm get_hfact_dup();


!p. fact(p) |-- fact(p) ** fact(p)


!p. fact(p) |-- fact(p) ** fact(p)

hsep_hfact_lefttheoremproof_kernel.h:260


thm get_hsep_hfact_left();


thm get_hsep_hfact_left();


!p hp1 hp2. (fact(p) ** hp1) ** hp2 -|- fact(p) ** (hp1 ** hp2)


!p hp1 hp2. (fact(p) ** hp1) ** hp2 -|- fact(p) ** (hp1 ** hp2)

hsep_hfact_righttheoremproof_kernel.h:263


thm get_hsep_hfact_right();


thm get_hsep_hfact_right();


!p hp1 hp2. hp1 ** (fact(p) ** hp2) -|- fact(p) ** (hp1 ** hp2)


!p hp1 hp2. hp1 ** (fact(p) ** hp2) -|- fact(p) ** (hp1 ** hp2)

hfact_defhfact_def 确定了两种嵌入之间的关系：fact(p)fact(p) 就是 pure(p) && emppure(p) && emp。 hfact_hpurehfact_hpure 则给出了实践中常用的形式：fact(p) ** hpfact(p) ** hp 与 pure(p) && hppure(p) && hp 是同一个命题。 hfact_duphfact_dup 是复制规则，它之所以健全，是因为纯事实不拥有任何资源。

在量词上的分配

**** 与 &&&& 如何与左侧或右侧的量词交互。涉及存在量词时，两边等价；涉及全称量词时，蕴含只在一个方向上成立。这种不对称符合预期：对分离合取的结果量化，弱于将量化后的命题作分离合取。

hsep_hexists_lefttheoremproof_kernel.h:266


thm get_hsep_hexists_left();


thm get_hsep_hexists_left();


!hpA hp. (exists x : A. hpA x) ** hp -|- exists x : A. (hpA x ** hp)


!hpA hp. (exists x : A. hpA x) ** hp -|- exists x : A. (hpA x ** hp)

hsep_hexists_righttheoremproof_kernel.h:269


thm get_hsep_hexists_right();


thm get_hsep_hexists_right();


!hp hpA. hp ** (exists x : A. hpA x) -|- exists x : A. (hp ** hpA x)


!hp hpA. hp ** (exists x : A. hpA x) -|- exists x : A. (hp ** hpA x)

hsep_hforall_lefttheoremproof_kernel.h:272


thm get_hsep_hforall_left();


thm get_hsep_hforall_left();


!hpA hp. (forall x : A. hpA x) ** hp |-- forall x : A. (hpA x ** hp)


!hpA hp. (forall x : A. hpA x) ** hp |-- forall x : A. (hpA x ** hp)

hsep_hforall_righttheoremproof_kernel.h:275


thm get_hsep_hforall_right();


thm get_hsep_hforall_right();


!hp hpA. hp ** (forall x : A. hpA x) |-- forall x : A. (hp ** hpA x)


!hp hpA. hp ** (forall x : A. hpA x) |-- forall x : A. (hp ** hpA x)

hand_hexists_lefttheoremproof_kernel.h:278


thm get_hand_hexists_left();


thm get_hand_hexists_left();


!hpA hp. (exists x : A. hpA x) && hp -|- exists x : A. (hpA x && hp)


!hpA hp. (exists x : A. hpA x) && hp -|- exists x : A. (hpA x && hp)

hand_hexists_righttheoremproof_kernel.h:281


thm get_hand_hexists_right();


thm get_hand_hexists_right();


!hp hpA. hp && (exists x : A. hpA x) -|- exists x : A. (hp && hpA x)


!hp hpA. hp && (exists x : A. hpA x) -|- exists x : A. (hp && hpA x)

hand_hforall_lefttheoremproof_kernel.h:284


thm get_hand_hforall_left();


thm get_hand_hforall_left();


!hpA hp. (forall x : A. hpA x) && hp |-- forall x : A. (hpA x && hp)


!hpA hp. (forall x : A. hpA x) && hp |-- forall x : A. (hpA x && hp)

hand_hforall_righttheoremproof_kernel.h:287


thm get_hand_hforall_right();


thm get_hand_hforall_right();


!hp hpA. hp && (forall x : A. hpA x) |-- forall x : A. (hp && hpA x)


!hp hpA. hp && (forall x : A. hpA x) |-- forall x : A. (hp && hpA x)

单调性

蕴含对量词与加性连接词的合同性，补全上文从 hsep_cancel_lefthsep_cancel_left 开始介绍的那组规则。

hexists_monotonetheoremproof_kernel.h:291


thm get_hexists_monotone();


thm get_hexists_monotone();


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((exists x:A. hpA x) |-- (exists x:A. hpA' x))


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((exists x:A. hpA x) |-- (exists x:A. hpA' x))

hforall_monotonetheoremproof_kernel.h:294


thm get_hforall_monotone();


thm get_hforall_monotone();


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((forall x:A. hpA x) |-- (forall x:A. hpA' x))


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((forall x:A. hpA x) |-- (forall x:A. hpA' x))

hand_monotonetheoremproof_kernel.h:297


thm get_hand_monotone();


thm get_hand_monotone();


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 && hp2 |-- hp1' && hp2')


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 && hp2 |-- hp1' && hp2')

hor_monotonetheoremproof_kernel.h:300


thm get_hor_monotone();


thm get_hor_monotone();


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 || hp2 |-- hp1' || hp2')


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 || hp2 |-- hp1' || hp2')

派生规则

有十个访问器带有 derivedderived 徽标，对应头文件中的 @derived@derived 标注。这个标注说明内核内部的证明层次：这些引理由上面的规则证明得到，并非直接从内存模型证明得到。它与信任程度无关。无论是否带有标注，访问器返回的都是证明器已经证明的定理，证明代码引用它们的方式也完全相同。

这些引理对应手工重排断言时常见的操作：把 factfact 交换到堆命题的另一侧，把三元 **** 的第二个合取项移到最前，或者将一条等价按当前需要的方向转换为蕴含。

hsep_hfalse_lefttheoremderivedproof_kernel.h:304


thm get_hsep_hfalse_left();


thm get_hsep_hfalse_left();


!hp. false ** hp |-- false


!hp. false ** hp |-- false

hsep_hfact_commtheoremderivedproof_kernel.h:308


thm get_hsep_hfact_comm();


thm get_hsep_hfact_comm();


!hp p. hp ** fact(p) -|- fact(p) ** hp


!hp p. hp ** fact(p) -|- fact(p) ** hp

hfact_hpure_righttheoremderivedproof_kernel.h:312


thm get_hfact_hpure_right();


thm get_hfact_hpure_right();


!p hp. hp && pure(p) -|- fact(p) ** hp


!p hp. hp && pure(p) -|- fact(p) ** hp

hsep_comm_left_parttheoremderivedproof_kernel.h:316


thm get_hsep_comm_left_part();


thm get_hsep_comm_left_part();


!hp hp1 hp2. hp1 ** hp ** hp2 -|- hp ** hp1 ** hp2


!hp hp1 hp2. hp1 ** hp ** hp2 -|- hp ** hp1 ** hp2

hentail_sym_lefttheoremderivedproof_kernel.h:320


thm get_hentail_sym_left();


thm get_hentail_sym_left();


!hp1 hp2. (hp1 -|- hp2) ==> (hp1 |-- hp2)


!hp1 hp2. (hp1 -|- hp2) ==> (hp1 |-- hp2)

hsep_cancel_left_eqtheoremderivedproof_kernel.h:324


thm get_hsep_cancel_left_eq();


thm get_hsep_cancel_left_eq();


!hp1 hp2 hp2'. (hp2 -|- hp2') ==> (hp1 ** hp2 -|- hp1 ** hp2')


!hp1 hp2 hp2'. (hp2 -|- hp2') ==> (hp1 ** hp2 -|- hp1 ** hp2')

hfact_elim_duptheoremderivedproof_kernel.h:328


thm get_hfact_elim_dup();


thm get_hfact_elim_dup();


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- fact(p) ** hp2)


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- fact(p) ** hp2)

hpure_add_hfacttheoremderivedproof_kernel.h:332


thm get_hpure_add_hfact();


thm get_hpure_add_hfact();


!p hp. (hp |-- pure(p)) ==> (hp |-- fact(p) ** hp)


!p hp. (hp |-- pure(p)) ==> (hp |-- fact(p) ** hp)

hsep_actheoremderivedproof_kernel.h:336


thm get_hsep_ac();


thm get_hsep_ac();


(hp1 ** hp2 -|- hp2 ** hp1) && ((hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)) && (hp1 ** (hp2 ** hp3) -|- hp2 ** (hp1 ** hp3))


(hp1 ** hp2 -|- hp2 ** hp1) && ((hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)) && (hp1 ** (hp2 ** hp3) -|- hp2 ** (hp1 ** hp3))

heq_symtheoremderivedproof_kernel.h:340


thm get_heq_sym();


thm get_heq_sym();


!hp1 hp2. (hp1 -|- hp2) <=> (hp2 -|- hp1)


!hp1 hp2. (hp1 -|- hp2) <=> (hp2 -|- hp1)

hsep_achsep_ac 汇集了三种嵌套 **** 的重排规则，用于依据结合律与交换律规范化。因此它的陈述是一个合取式，而不是单条等价。

C 类型、sizeof 与取值范围

四个访问器与 :ctype:ctype 索引有关：在标量类型上确定 sizeofsizeof、min_ofmin_of 与 max_ofmax_of 的方程，外加内核直接导出的那一条推论。

sizeof_deftheoremproof_kernel.h:373


thm get_sizeof_def();


thm get_sizeof_def();


the definition of `sizeof : ctype->int


the definition of `sizeof : ctype->int

sizeof_ge_0theoremproof_kernel.h:376


thm get_sizeof_ge_0();


thm get_sizeof_ge_0();


!ty. sizeof ty >= &0


!ty. sizeof ty >= &0

min_of_deftheoremproof_kernel.h:379


thm get_min_of_def();


thm get_min_of_def();


the definition of `min_of : ctype->int


the definition of `min_of : ctype->int

max_of_deftheoremproof_kernel.h:382


thm get_max_of_def();


thm get_max_of_def();


the definition of `max_of : ctype->int


the definition of `max_of : ctype->int

注释中的 the definition of ff 表示访问器返回定义定理，即各标量构造子的方程组成的合取式。重写时正是用这些方程将 sizeof Tintsizeof Tint 计算为数值字面量。 sizeof_ge_0sizeof_ge_0 表达的是任何 C 类型的大小都不为负这一事实，凡是需要给数组地址 x + i * sizeof(ty)x + i * sizeof(ty) 定界的地方都会用到它。

类型形态、指针有效性与对齐

这里列出带类型存储单元的有效性条件所用的定义，以及这些定义所依赖的对齐谓词的代数性质。is_scalar_ctypeis_scalar_ctype 是把九个标量构造子（以及标量类型的 TaliasTalias 别名）与复合类型区分开来的附加条件；aligned_n n xaligned_n n x 表示 xx 是 nn 的整数倍；五个 isvalidptr*isvalidptr* 谓词结合了地址空间边界条件与相应存储宽度所需的对齐条件，其中 isvalidptr_charisvalidptr_char 没有对齐要求。十二条 aligned_n_*aligned_n_* 引理都以变量表示模数，因此每条引理都适用于任意对齐要求。

is_scalar_ctype_deftheoremproof_kernel.h:388


thm get_is_scalar_ctype_def();


thm get_is_scalar_ctype_def();


the definition of `is_scalar_ctype : ctype->bool


the definition of `is_scalar_ctype : ctype->bool

aligned_n_deftheoremproof_kernel.h:391


thm get_aligned_n_def();


thm get_aligned_n_def();


the definition of `aligned_n : int->int->bool


the definition of `aligned_n : int->int->bool

isvalidptr_char_deftheoremproof_kernel.h:394


thm get_isvalidptr_char_def();


thm get_isvalidptr_char_def();


the definition of `isvalidptr_char : int->bool


the definition of `isvalidptr_char : int->bool

isvalidptr_short_deftheoremproof_kernel.h:397


thm get_isvalidptr_short_def();


thm get_isvalidptr_short_def();


the definition of `isvalidptr_short : int->bool


the definition of `isvalidptr_short : int->bool

isvalidptr_int_deftheoremproof_kernel.h:400


thm get_isvalidptr_int_def();


thm get_isvalidptr_int_def();


the definition of `isvalidptr_int : int->bool


the definition of `isvalidptr_int : int->bool

isvalidptr_int64_deftheoremproof_kernel.h:403


thm get_isvalidptr_int64_def();


thm get_isvalidptr_int64_def();


the definition of `isvalidptr_int64 : int->bool


the definition of `isvalidptr_int64 : int->bool

isvalidptr_deftheoremproof_kernel.h:406


thm get_isvalidptr_def();


thm get_isvalidptr_def();


the definition of `isvalidptr : int->bool


the definition of `isvalidptr : int->bool

aligned_n_addtheoremproof_kernel.h:409


thm get_aligned_n_add();


thm get_aligned_n_add();


!n x y. aligned_n n x ==> aligned_n n y ==> aligned_n n (x + y)


!n x y. aligned_n n x ==> aligned_n n y ==> aligned_n n (x + y)

aligned_n_subtheoremproof_kernel.h:412


thm get_aligned_n_sub();


thm get_aligned_n_sub();


!n x y. aligned_n n x ==> aligned_n n y ==> aligned_n n (x - y)


!n x y. aligned_n n x ==> aligned_n n y ==> aligned_n n (x - y)

aligned_n_negtheoremproof_kernel.h:415


thm get_aligned_n_neg();


thm get_aligned_n_neg();


!n x. aligned_n n x ==> aligned_n n (--x)


!n x. aligned_n n x ==> aligned_n n (--x)

aligned_n_multheoremproof_kernel.h:418


thm get_aligned_n_mul();


thm get_aligned_n_mul();


!n k. aligned_n n (n * k)


!n k. aligned_n n (n * k)

aligned_n_mul_lefttheoremproof_kernel.h:421


thm get_aligned_n_mul_left();


thm get_aligned_n_mul_left();


!n k. aligned_n n (k * n)


!n k. aligned_n n (k * n)

aligned_n_add_multheoremproof_kernel.h:424


thm get_aligned_n_add_mul();


thm get_aligned_n_add_mul();


!n x k. aligned_n n x ==> aligned_n n (x + n * k)


!n x k. aligned_n n x ==> aligned_n n (x + n * k)

aligned_n_add_mul_lefttheoremproof_kernel.h:427


thm get_aligned_n_add_mul_left();


thm get_aligned_n_add_mul_left();


!n x k. aligned_n n x ==> aligned_n n (x + k * n)


!n x k. aligned_n n x ==> aligned_n n (x + k * n)

aligned_n_refltheoremproof_kernel.h:430


thm get_aligned_n_refl();


thm get_aligned_n_refl();


!n. aligned_n n n


!n. aligned_n n n

aligned_n_zerotheoremproof_kernel.h:433


thm get_aligned_n_zero();


thm get_aligned_n_zero();


!n. aligned_n n (&0)


!n. aligned_n n (&0)

aligned_n_onetheoremproof_kernel.h:436


thm get_aligned_n_one();


thm get_aligned_n_one();


!x. aligned_n (&1) x


!x. aligned_n (&1) x

aligned_n_mult_oftheoremproof_kernel.h:439


thm get_aligned_n_mult_of();


thm get_aligned_n_mult_of();


!n m x. aligned_n (n * m) x ==> aligned_n n x


!n m x. aligned_n (n * m) x ==> aligned_n n x

aligned_n_remtheoremproof_kernel.h:442


thm get_aligned_n_rem();


thm get_aligned_n_rem();


!n x. aligned_n n x <=> x rem n = &0


!n x. aligned_n n x <=> x rem n = &0

这些引理按名称注册，供证明代码获取和匹配。int_arith_ruleint_arith_rule 将 aligned_naligned_n 视为不透明的原子，因此证明中会保留对齐事实，并用这些规则组合它们，无需重新推导。当模数是数值字面量、用算术推理更方便时，可以用 aligned_n_remaligned_n_rem 在对齐谓词与 x rem n = &0x rem n = &0 之间转换。带类型的内存谓词页说明这些谓词的含义以及它们出现在何处。

带类型的存储单元与数组定义

data_atdata_at 与 undef_data_atundef_data_at 是描述单个带类型存储单元的内存谓词。下面先列出关于它们的四条规则，再列出数组谓词的六条定义定理。

data_at_to_undef_data_attheoremproof_kernel.h:445


thm get_data_at_to_undef_data_at();


thm get_data_at_to_undef_data_at();


!x ty v. data_at x ty v |-- undef_data_at x ty


!x ty v. data_at x ty v |-- undef_data_at x ty

data_at_rangetheoremproof_kernel.h:448


thm get_data_at_range();


thm get_data_at_range();


!x ty v. data_at x ty v |-- data_at x ty v ** fact(min_of(ty) <= v && v <= max_of(ty))


!x ty v. data_at x ty v |-- data_at x ty v ** fact(min_of(ty) <= v && v <= max_of(ty))

data_at_duptheoremproof_kernel.h:451


thm get_data_at_dup();


thm get_data_at_dup();


!x ty v1 v2. data_at x ty v1 ** data_at x ty v2 |-- false


!x ty v1 v2. data_at x ty v1 ** data_at x ty v2 |-- false

undef_data_at_duptheoremproof_kernel.h:454


thm get_undef_data_at_dup();


thm get_undef_data_at_dup();


!x ty. undef_data_at x ty ** undef_data_at x ty |-- false


!x ty. undef_data_at x ty ** undef_data_at x ty |-- false

array_at_rec_deftheoremproof_kernel.h:457


thm get_array_at_rec_def();


thm get_array_at_rec_def();


the definition of `array_at_rec : addr->ctype->int->int->(int)list->hprop


the definition of `array_at_rec : addr->ctype->int->int->(int)list->hprop

array_at_missing_i_rec_deftheoremproof_kernel.h:460


thm get_array_at_missing_i_rec_def();


thm get_array_at_missing_i_rec_def();


the definition of `array_at_missing_i_rec : addr->ctype->int->int->int->(int)list->hprop


the definition of `array_at_missing_i_rec : addr->ctype->int->int->int->(int)list->hprop

array_at_deftheoremproof_kernel.h:463


thm get_array_at_def();


thm get_array_at_def();


the definition of `array_at : addr->ctype->int->(int)list->hprop


the definition of `array_at : addr->ctype->int->(int)list->hprop

undef_array_at_rec_deftheoremproof_kernel.h:466


thm get_undef_array_at_rec_def();


thm get_undef_array_at_rec_def();


the definition of `undef_array_at_rec : addr->ctype->int->int->num->hprop


the definition of `undef_array_at_rec : addr->ctype->int->int->num->hprop

undef_array_at_missing_i_rec_deftheoremproof_kernel.h:469


thm get_undef_array_at_missing_i_rec_def();


thm get_undef_array_at_missing_i_rec_def();


the definition of `undef_array_at_missing_i_rec : addr->ctype->int->int->int->num->hprop


the definition of `undef_array_at_missing_i_rec : addr->ctype->int->int->int->num->hprop

undef_array_at_deftheoremproof_kernel.h:472


thm get_undef_array_at_def();


thm get_undef_array_at_def();


the definition of `undef_array_at : addr->ctype->int->hprop


the definition of `undef_array_at : addr->ctype->int->hprop

data_at_rangedata_at_range 体现了类型索引的作用：存储的值总在 min_of(ty)min_of(ty) 与 max_of(ty)max_of(ty) 之间。这条规则将这一范围条件作为纯事实提供出来，同时保留该存储单元。 data_at_dupdata_at_dup 与 undef_data_at_dupundef_data_at_dup 是反复制事实，使所有权具有排他性：对同一地址的两份声明蕴含 falsefalse。

带 _def_def 的条目返回的是定义，其注释给出的是被定义谓词的签名，而不是方程。带 _rec_rec 的变体接受显式的索引范围 lolo、hihi；不带后缀的 array_atarray_at 在这些变体的基础上，以长度为索引；带 missing_imissing_i 的变体描述从数组中切出索引 ii 处的单元后剩余的部分。

列表操作

数组内容是 HOL 列表，因此内核导出了表述数组规则所需的列表操作。LENGTHLENGTH、MEMMEM、 APPENDAPPEND、REVERSEREVERSE 与 REPLICATEREPLICATE 是 HOL Light 自带的；以 II 为前缀的操作—— ilengthilength、inthinth、ifirstnifirstn、iskipniskipn、ireplicateireplicate、replace_inthreplace_inth、sublistsublist——是 C* 提供的相应操作，采用整数索引，使列表下标与 C 的整数运算使用同一个类型。

LENGTHtheoremproof_kernel.h:475


thm get_LENGTH();


thm get_LENGTH();


LENGTH [] = 0 /\ (!h t. LENGTH (CONS h t) = SUC (LENGTH t))


LENGTH [] = 0 /\ (!h t. LENGTH (CONS h t) = SUC (LENGTH t))

ILENGTH_DEFtheoremproof_kernel.h:478


thm get_ILENGTH_DEF();


thm get_ILENGTH_DEF();


the definition of `ilength : (A)list->int


the definition of `ilength : (A)list->int

NTH_DEFtheoremproof_kernel.h:481


thm get_NTH_DEF();


thm get_NTH_DEF();


the definition of `NTH : num->(A)list->A


the definition of `NTH : num->(A)list->A

INTH_DEFtheoremproof_kernel.h:484


thm get_INTH_DEF();


thm get_INTH_DEF();


the definition of `inth : int->(A)list->A


the definition of `inth : int->(A)list->A

REPLACE_NTH_DEFtheoremproof_kernel.h:487


thm get_REPLACE_NTH_DEF();


thm get_REPLACE_NTH_DEF();


the definition of `REPLACE_NTH : num->A->(A)list->(A)list


the definition of `REPLACE_NTH : num->A->(A)list->(A)list

REPLACE_INTH_DEFtheoremproof_kernel.h:490


thm get_REPLACE_INTH_DEF();


thm get_REPLACE_INTH_DEF();


the definition of `replace_inth : int->A->(A)list->(A)list


the definition of `replace_inth : int->A->(A)list->(A)list

FIRSTN_DEFtheoremproof_kernel.h:493


thm get_FIRSTN_DEF();


thm get_FIRSTN_DEF();


the definition of `FIRSTN : num->(A)list->(A)list


the definition of `FIRSTN : num->(A)list->(A)list

IFIRSTN_DEFtheoremproof_kernel.h:496


thm get_IFIRSTN_DEF();


thm get_IFIRSTN_DEF();


the definition of `ifirstn : int->(A)list->(A)list


the definition of `ifirstn : int->(A)list->(A)list

SKIPN_DEFtheoremproof_kernel.h:499


thm get_SKIPN_DEF();


thm get_SKIPN_DEF();


the definition of `SKIPN : num->(A)list->(A)list


the definition of `SKIPN : num->(A)list->(A)list

ISKIPN_DEFtheoremproof_kernel.h:502


thm get_ISKIPN_DEF();


thm get_ISKIPN_DEF();


the definition of `iskipn : int->(A)list->(A)list


the definition of `iskipn : int->(A)list->(A)list

REPLICATEtheoremproof_kernel.h:505


thm get_REPLICATE();


thm get_REPLICATE();


REPLICATE 0 x = [] /\ REPLICATE (SUC n) x = CONS x (REPLICATE n x)


REPLICATE 0 x = [] /\ REPLICATE (SUC n) x = CONS x (REPLICATE n x)

IREPLICATE_DEFtheoremproof_kernel.h:508


thm get_IREPLICATE_DEF();


thm get_IREPLICATE_DEF();


the definition of `ireplicate : int->A->(A)list


the definition of `ireplicate : int->A->(A)list

SUBLIST_DEFtheoremproof_kernel.h:511


thm get_SUBLIST_DEF();


thm get_SUBLIST_DEF();


the definition of `sublist : int->int->(A)list->(A)list


the definition of `sublist : int->int->(A)list->(A)list

MEMtheoremproof_kernel.h:514


thm get_MEM();


thm get_MEM();


(MEM x [] <=> F) /\ (MEM x (CONS h t) <=> x = h \/ MEM x t)


(MEM x [] <=> F) /\ (MEM x (CONS h t) <=> x = h \/ MEM x t)

APPENDtheoremproof_kernel.h:517


thm get_APPEND();


thm get_APPEND();


(!l. APPEND [] l = l) /\ (!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))


(!l. APPEND [] l = l) /\ (!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))

REVERSEtheoremproof_kernel.h:520


thm get_REVERSE();


thm get_REVERSE();


REVERSE [] = [] /\ REVERSE (CONS x l) = APPEND (REVERSE l) [x]


REVERSE [] = [] /\ REVERSE (CONS x l) = APPEND (REVERSE l) [x]

ILENGTH_NONNEGtheoremproof_kernel.h:523


thm get_ILENGTH_NONNEG();


thm get_ILENGTH_NONNEG();


!l:(A)list. &0 <= ilength l


!l:(A)list. &0 <= ilength l

ILENGTH_APPENDtheoremproof_kernel.h:526


thm get_ILENGTH_APPEND();


thm get_ILENGTH_APPEND();


!l1:(A)list l2:(A)list. ilength(l1 ++ l2) == ilength(l1) + ilength(l2)


!l1:(A)list l2:(A)list. ilength(l1 ++ l2) == ilength(l1) + ilength(l2)

ISKIPN_SPLIT_FIRSTtheoremproof_kernel.h:529


thm get_ISKIPN_SPLIT_FIRST();


thm get_ISKIPN_SPLIT_FIRST();


!i:int l:(A)list. &0 <= i && i < ilength l ==> iskipn i l == (inth i l) :: (iskipn (i + &1) l)


!i:int l:(A)list. &0 <= i && i < ilength l ==> iskipn i l == (inth i l) :: (iskipn (i + &1) l)

ISKIPN_ILENGTHtheoremproof_kernel.h:532


thm get_ISKIPN_ILENGTH();


thm get_ISKIPN_ILENGTH();


!l:(A)list. iskipn (ilength l) l == []


!l:(A)list. iskipn (ilength l) l == []

ILENGTH_IREPLICATEtheoremproof_kernel.h:535


thm get_ILENGTH_IREPLICATE();


thm get_ILENGTH_IREPLICATE();


!n:int v:A. &0 <= n ==> ilength(ireplicate n v) == n


!n:int v:A. &0 <= n ==> ilength(ireplicate n v) == n

IREPLICATE_APPENDtheoremproof_kernel.h:538


thm get_IREPLICATE_APPEND();


thm get_IREPLICATE_APPEND();


!n:int v:A. &0 <= n ==> (ireplicate n v) ++ [v] == ireplicate (n + &1) v


!n:int v:A. &0 <= n ==> (ireplicate n v) ++ [v] == ireplicate (n + &1) v

最后六条给出数组推理常用的已证事实：ilengthilength 非负且对拼接可加，从非空后缀的前端跳过一个元素的行为符合预期，跳过全部长度后得到空列表，以及填充未初始化数组时用到的两条关于 ireplicateireplicate 的事实。

array_at 规则族

这三十条规则支持数组推理：长度与范围事实，从数组中切分出一个单元再合并回去，在头部或尾部操作，重设索引范围的基址，把数组一分为二，以及空数组的情形。每条都有已初始化的 array_atarray_at 形式，并在适用时配有相应的 undef_array_atundef_array_at 形式。

array_at_rec_lengththeoremproof_kernel.h:541


thm get_array_at_rec_length();


thm get_array_at_rec_length();


!x ty lo hi l. array_at_rec x ty lo hi l |-- array_at_rec x ty lo hi l ** fact(ilength(l) == hi - lo)


!x ty lo hi l. array_at_rec x ty lo hi l |-- array_at_rec x ty lo hi l ** fact(ilength(l) == hi - lo)

array_at_lengththeoremproof_kernel.h:544


thm get_array_at_length();


thm get_array_at_length();


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(ilength(l) == n)


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(ilength(l) == n)

array_at_rangetheoremproof_kernel.h:547


thm get_array_at_range();


thm get_array_at_range();


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(!i. &0 <= i ==> i < n ==> (min_of(ty) <= inth i l && inth i l <= max_of(ty)))


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(!i. &0 <= i ==> i < n ==> (min_of(ty) <= inth i l && inth i l <= max_of(ty)))

array_at_rec_splittheoremproof_kernel.h:550


thm get_array_at_rec_split();


thm get_array_at_rec_split();


!x ty lo n m l. (lo <= n) ==> (n < m) ==> (array_at_rec x ty lo m l |-- data_at (x + n * sizeof(ty)) ty (inth (n - lo) l) ** array_at_missing_i_rec x ty n lo m l)


!x ty lo n m l. (lo <= n) ==> (n < m) ==> (array_at_rec x ty lo m l |-- data_at (x + n * sizeof(ty)) ty (inth (n - lo) l) ** array_at_missing_i_rec x ty n lo m l)

array_at_splittheoremproof_kernel.h:553


thm get_array_at_split();


thm get_array_at_split();


!x ty n m l. (&0 <= n) ==> (n < m) ==> (array_at x ty m l |-- data_at (x + n * sizeof(ty)) ty (inth n l) ** array_at_missing_i_rec x ty n (&0) m l)


!x ty n m l. (&0 <= n) ==> (n < m) ==> (array_at x ty m l |-- data_at (x + n * sizeof(ty)) ty (inth n l) ** array_at_missing_i_rec x ty n (&0) m l)

array_at_rec_mergetheoremproof_kernel.h:556


thm get_array_at_rec_merge();


thm get_array_at_rec_merge();


!x ty lo n m a l. (lo <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n lo m l |-- array_at_rec x ty lo m (replace_inth (n - lo) a l))


!x ty lo n m a l. (lo <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n lo m l |-- array_at_rec x ty lo m (replace_inth (n - lo) a l))

array_at_mergetheoremproof_kernel.h:559


thm get_array_at_merge();


thm get_array_at_merge();


!x ty n m a l. (&0 <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n (&0) m l |-- array_at x ty m (replace_inth n a l))


!x ty n m a l. (&0 <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n (&0) m l |-- array_at x ty m (replace_inth n a l))

array_at_rec_headtheoremproof_kernel.h:562


thm get_array_at_rec_head();


thm get_array_at_rec_head();


!x ty lo hi l. (lo < hi) ==> (array_at_rec x ty lo hi l |-- data_at (x + lo * sizeof(ty)) ty (inth (&0) l) ** array_at_rec x ty (lo + &1) hi (sublist (&1) (hi - lo) l))


!x ty lo hi l. (lo < hi) ==> (array_at_rec x ty lo hi l |-- data_at (x + lo * sizeof(ty)) ty (inth (&0) l) ** array_at_rec x ty (lo + &1) hi (sublist (&1) (hi - lo) l))

array_at_rec_head_mergetheoremproof_kernel.h:565


thm get_array_at_rec_head_merge();


thm get_array_at_rec_head_merge();


!x ty lo hi a l. (lo < hi) ==> (data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l |-- array_at_rec x ty lo hi (a :: l))


!x ty lo hi a l. (lo < hi) ==> (data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l |-- array_at_rec x ty lo hi (a :: l))

array_at_array_rec_constheoremproof_kernel.h:568


thm get_array_at_array_rec_cons();


thm get_array_at_array_rec_cons();


!x ty lo hi a l. (lo < hi) ==> (array_at_rec x ty lo hi (a :: l) |-- data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l)


!x ty lo hi a l. (lo < hi) ==> (array_at_rec x ty lo hi (a :: l) |-- data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l)

array_at_rec_tail_mergetheoremproof_kernel.h:571


thm get_array_at_rec_tail_merge();


thm get_array_at_rec_tail_merge();


!x ty lo hi a l. (lo <= hi) ==> (data_at (x + hi * sizeof(ty)) ty a ** array_at_rec x ty lo hi l |-- array_at_rec x ty lo (hi + &1) (l ++ [a]))


!x ty lo hi a l. (lo <= hi) ==> (data_at (x + hi * sizeof(ty)) ty a ** array_at_rec x ty lo hi l |-- array_at_rec x ty lo (hi + &1) (l ++ [a]))

array_at_rec_basetheoremproof_kernel.h:574


thm get_array_at_rec_base();


thm get_array_at_rec_base();


!x ty m k n l. array_at_rec x ty (m + k) n l -|- array_at_rec (x + k * sizeof(ty)) ty m (n - k) l


!x ty m k n l. array_at_rec x ty (m + k) n l -|- array_at_rec (x + k * sizeof(ty)) ty m (n - k) l

array_at_rec_divide_auxtheoremproof_kernel.h:577


thm get_array_at_rec_divide_aux();


thm get_array_at_rec_divide_aux();


!x ty lo m n l. (lo <= m) ==> (m <= n) ==> (ilength(l) == n - lo) ==> (array_at_rec x ty lo n l -|- array_at_rec x ty lo m (sublist (&0) (m - lo) l) ** array_at_rec x ty m n (sublist (m - lo) (n - lo) l))


!x ty lo m n l. (lo <= m) ==> (m <= n) ==> (ilength(l) == n - lo) ==> (array_at_rec x ty lo n l -|- array_at_rec x ty lo m (sublist (&0) (m - lo) l) ** array_at_rec x ty m n (sublist (m - lo) (n - lo) l))

array_at_rec_dividetheoremproof_kernel.h:580


thm get_array_at_rec_divide();


thm get_array_at_rec_divide();


!x ty m n l. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at_rec x ty (&0) n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))


!x ty m n l. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at_rec x ty (&0) n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

array_at_dividetheoremproof_kernel.h:583


thm get_array_at_divide();


thm get_array_at_divide();


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at x ty m (sublist (&0) m l) ** array_at (x + m * sizeof(ty)) ty (n - m) (sublist m n l))


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at x ty m (sublist (&0) m l) ** array_at (x + m * sizeof(ty)) ty (n - m) (sublist m n l))

array_at_divide2theoremproof_kernel.h:586


thm get_array_at_divide2();


thm get_array_at_divide2();


!x ty n m l1 l2. (ilength(l1) == n) ==> (ilength(l2) == m) ==> (array_at x ty (n + m) (l1 ++ l2) -|- array_at x ty n l1 ** array_at (x + n * sizeof(ty)) ty m l2)


!x ty n m l1 l2. (ilength(l1) == n) ==> (ilength(l2) == m) ==> (array_at x ty (n + m) (l1 ++ l2) -|- array_at x ty n l1 ** array_at (x + n * sizeof(ty)) ty m l2)

array_at_divide_rectheoremproof_kernel.h:589


thm get_array_at_divide_rec();


thm get_array_at_divide_rec();


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

undef_array_at_rec_basetheoremproof_kernel.h:592


thm get_undef_array_at_rec_base();


thm get_undef_array_at_rec_base();


!x ty m k n len. undef_array_at_rec x ty (m + k) n len -|- undef_array_at_rec (x + k * sizeof(ty)) ty m (n - k) len


!x ty m k n len. undef_array_at_rec x ty (m + k) n len -|- undef_array_at_rec (x + k * sizeof(ty)) ty m (n - k) len

undef_array_at_dividetheoremproof_kernel.h:595


thm get_undef_array_at_divide();


thm get_undef_array_at_divide();


!x ty n m. (&0 <= m) ==> (m <= n) ==> (undef_array_at x ty n -|- undef_array_at x ty m ** undef_array_at (x + m * sizeof(ty)) ty (n - m))


!x ty n m. (&0 <= m) ==> (m <= n) ==> (undef_array_at x ty n -|- undef_array_at x ty m ** undef_array_at (x + m * sizeof(ty)) ty (n - m))

undef_Tuchar_array_at_splittheoremproof_kernel.h:598


thm get_undef_Tuchar_array_at_split();


thm get_undef_Tuchar_array_at_split();


!x ty n. is_scalar_ctype ty ==> aligned_n (sizeof(ty)) x ==> n >= sizeof(ty) ==> (undef_array_at x Tuchar n -|- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) Tuchar (n - sizeof(ty)))


!x ty n. is_scalar_ctype ty ==> aligned_n (sizeof(ty)) x ==> n >= sizeof(ty) ==> (undef_array_at x Tuchar n -|- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) Tuchar (n - sizeof(ty)))

array_at_split_firsttheoremproof_kernel.h:601


thm get_array_at_split_first();


thm get_array_at_split_first();


!x ty n v l. (n >= &1) ==> (array_at x ty n (v :: l) |-- data_at x ty v ** array_at (x + sizeof(ty)) ty (n - &1) l)


!x ty n v l. (n >= &1) ==> (array_at x ty n (v :: l) |-- data_at x ty v ** array_at (x + sizeof(ty)) ty (n - &1) l)

array_at_merge_firsttheoremproof_kernel.h:604


thm get_array_at_merge_first();


thm get_array_at_merge_first();


!x ty n v l. data_at x ty v ** array_at (x + sizeof(ty)) ty n l |-- array_at x ty (n + &1) (v :: l)


!x ty n v l. data_at x ty v ** array_at (x + sizeof(ty)) ty n l |-- array_at x ty (n + &1) (v :: l)

array_at_split_lasttheoremproof_kernel.h:607


thm get_array_at_split_last();


thm get_array_at_split_last();


!x ty n v l. (n >= &1) ==> (array_at x ty n (l ++ [v]) |-- array_at x ty (n - &1) l ** data_at (x + (n - &1) * sizeof(ty)) ty v)


!x ty n v l. (n >= &1) ==> (array_at x ty n (l ++ [v]) |-- array_at x ty (n - &1) l ** data_at (x + (n - &1) * sizeof(ty)) ty v)

array_at_merge_lasttheoremproof_kernel.h:610


thm get_array_at_merge_last();


thm get_array_at_merge_last();


!x ty n v l. array_at x ty n l ** data_at (x + n * sizeof(ty)) ty v |-- array_at x ty (n + &1) (l ++ [v])


!x ty n v l. array_at x ty n l ** data_at (x + n * sizeof(ty)) ty v |-- array_at x ty (n + &1) (l ++ [v])

undef_array_at_split_firsttheoremproof_kernel.h:613


thm get_undef_array_at_split_first();


thm get_undef_array_at_split_first();


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty (n - &1))


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty (n - &1))

undef_array_at_merge_firsttheoremproof_kernel.h:616


thm get_undef_array_at_merge_first();


thm get_undef_array_at_merge_first();


!x ty n. undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty n |-- undef_array_at x ty (n + &1)


!x ty n. undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty n |-- undef_array_at x ty (n + &1)

undef_array_at_split_lasttheoremproof_kernel.h:619


thm get_undef_array_at_split_last();


thm get_undef_array_at_split_last();


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_array_at x ty (n - &1) ** undef_data_at (x + (n - &1) * sizeof(ty)) ty)


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_array_at x ty (n - &1) ** undef_data_at (x + (n - &1) * sizeof(ty)) ty)

undef_array_at_merge_lasttheoremproof_kernel.h:622


thm get_undef_array_at_merge_last();


thm get_undef_array_at_merge_last();


!x ty n. undef_array_at x ty n ** undef_data_at (x + n * sizeof(ty)) ty |-- undef_array_at x ty (n + &1)


!x ty n. undef_array_at x ty n ** undef_data_at (x + n * sizeof(ty)) ty |-- undef_array_at x ty (n + &1)

array_at_zerotheoremproof_kernel.h:625


thm get_array_at_zero();


thm get_array_at_zero();


!x ty n l. (n == &0) ==> (l == []) ==> (array_at x ty n l -|- emp)


!x ty n l. (n == &0) ==> (l == []) ==> (array_at x ty n l -|- emp)

undef_array_at_zerotheoremproof_kernel.h:628


thm get_undef_array_at_zero();


thm get_undef_array_at_zero();


!x ty n. (n == &0) ==> (undef_array_at x ty n -|- emp)


!x ty n. (n == &0) ==> (undef_array_at x ty n -|- emp)

这些规则遵循同一条寻址约定：以 xx 为基址、元素类型为 tyty 的数组，其第 ii 个元素位于 x + i * sizeof(ty)x + i * sizeof(ty)。带类型的内存谓词页按作用对同一批规则重新分组，并逐条讲解循环不变式实际需要的规则。

小结

proof_kernel.hproof_kernel.h 声明了十个不透明句柄类型与六个列表别名、三个实现访问器约定的宏、三十三个面向逻辑内置项与内置类型的访问器，以及一百六十个定理访问器。内核中名为 TT 的定理在 C 侧就是 get_T()get_T()；对象只从证明器取回一次，并在此后的整个运行过程中缓存。

这些接口涵盖了证明代码获取逻辑内置对象的全部途径。获取对象之后的操作，包括匹配、实例化、重写和卸除，都属于证明器 API；引擎使用这些结果的操作则属于符号执行 API。