证明自动化

前几部分让证明更短、更可复用：后向策略分解给定的待证目标，操作逐项打包资源变换，胶囊则把代码连同其证明打包在一起。 但它们都没有改变谁在做这些工作：在每个程序点上，仍然要由人来决定哪个内存单元匹配哪个、读取前展开哪个链表，以及还剩哪条等式需要证明。 把几个这样的证明放在一起对照就会发现，相同的动作在不断重复——为每个程序变量的 data_atdata_at 配对、展开一个链表节点、再折叠回去，最后以一条简单的列表等式或整数边界收尾。

本部分把这些例行工作自动化。

用策略纯化蕴含负责空间推理这一半的自动化。 它引入策略（strategy）——描述 sllsll 这类谓词如何展开、折叠与消去的声明式规则——以及 PURIFY_TACPURIFY_TAC：反复应用这些规则，直到蕴含中不再含有空间资源；再加上把纯化后目标转换为普通逻辑公式的 POST_PURIFY_TACPOST_PURIFY_TAC。 同一套策略还会定制符号执行引擎在内存读写处执行框架推断（frame inference）的方式；该节最后以数组谓词的策略收尾。

用 SMT 求解纯目标负责纯推理这一半的自动化。 它把 C* 的证明层连接到 Z3 SMT 求解器：SMT_TACSMT_TAC 求解普通逻辑目标，smt_add_axiomsmt_add_axiom 把已证明的列表定理作为背景知识提供给求解器，而对 term_to_z3term_to_z3 的简要考察则展示 HOL 项如何翻译——以及翻译在何处止步。 与纯化结合，就得到三步流水线 solve_vc_autosolve_vc_auto，并在反转与数组两个示例上完整展示其效果。