证明自动化

前几部分缩短了证明，也让证明更易复用：后向策略分解给定的待证目标，每个操作封装一次资源变换，胶囊则将代码与相应的证明封装在一起。不过，这些方法都没有改变谁来完成证明：在每个程序点上，仍然要由人来决定内存单元之间如何匹配、读取前要展开哪个链表，以及还剩哪条等式需要证明。对照几个这样的证明，就会发现其中反复出现相同的步骤：为每个程序变量的 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。该节通过链表反转与数组清零两个示例，完整展示它的使用过程。

用 cstar_mcp 进行 AI 辅助验证把剩下的判断交给助手。该节介绍 cstar_mcpcstar_mcp 服务器，它通过 Model Context Protocol 提供验证器的访问接口。该节说明服务器的注册方法、助手可用的六个工具和助手执行的验证回路，并给出围绕 twicetwice 示例展开的一次简短会话。