C*：开发与证明一体化

分离逻辑的后向证明

EN | 中文

前一节将目标统一写为 [Gamma ?- p][Gamma ?- p]，策略通过目标树将一个普通布尔命题分解为子目标。但 C* 的验证条件通常是分离逻辑蕴含：证明器不仅要处理命题，还必须拆分、选择和重组线性堆资源。本节在前一节通用目标树的基础上，介绍专门处理这类资源的目标表示与策略族，并结合前文介绍的 sllsll 谓词展开讨论。

我们围绕链表逆置例子中的一个引理展开讨论。在前向证明一节中，我们将 sll_unfoldsll_unfold 作为现成的定理复用；现在来证明这个引理，本节将其称为 unfold_sll_not_nullunfold_sll_not_null。

先回顾单向链表谓词 sll pt lsll pt l，它描述一个从地址 ptpt 开始的链表，其逻辑内容是整数列表 ll：

// struct list { int head; struct list *tail; }，Tlist、Fhead、Ftail
// 按“C* 中的分离逻辑”一节的方式注册
PROOF thm sll_def = cst_new_rec_definition(
  "sll", get_theorem_by_name("list_RECURSION"),
  `(sll pt [] -|- fact(pt == 0i)) &&
   (sll pt (h :: t) -|- fact(~(pt == 0i)) ** exists q.
      data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr q ** sll q t)`,
  `:addr->(int)list->hprop`);
// struct list { int head; struct list *tail; }，Tlist、Fhead、Ftail
// 按“C* 中的分离逻辑”一节的方式注册
PROOF thm sll_def = cst_new_rec_definition(
  "sll", get_theorem_by_name("list_RECURSION"),
  `(sll pt [] -|- fact(pt == 0i)) &&
   (sll pt (h :: t) -|- fact(~(pt == 0i)) ** exists q.
      data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr q ** sll q t)`,
  `:addr->(int)list->hprop`);

空链表用空指针表示；非空链表的头节点拥有 headhead 和 tailtail 字段，尾指针 qq 指向表示剩余列表 tt 的链表。 cst_new_rec_definitioncst_new_rec_definition 是示例用户库（userlib/qcp/veriftime.huserlib/qcp/veriftime.h）中的辅助函数：一次调用就能完成递归定义，并将新常量导出给引擎；PROOFPROOF 是标准库为 [[cst::proof]][[cst::proof]] 提供的简写。

引理 1（unfold_sll_not_nullunfold_sll_not_null）。

如果 ptpt 非空且 sll pt lsll pt l 成立，那么 ll 必定具有 h :: th :: t 的形式，展开头节点后得到两个字段资源和一个后继链表：

forall l pt.
  ~(pt == 0i)
  ==> (sll pt l |--
        exists h t q.
          fact(l == h :: t) **
          data_at (field_addr pt Tlist Fhead) Tint h **
          data_at (field_addr pt Tlist Ftail) Tptr q **
          sll q t)
forall l pt.
  ~(pt == 0i)
  ==> (sll pt l |--
        exists h t q.
          fact(l == h :: t) **
          data_at (field_addr pt Tlist Fhead) Tint h **
          data_at (field_addr pt Tlist Ftail) Tptr q **
          sll q t)

这个引理看起来只需“展开一次定义”，实际证明却包含几个不同的步骤：先引入全称量词和纯前件 ~(pt == 0i)~(pt == 0i)，将 sll pt l |-- ...sll pt l |-- ... 转为适合操作资源的目标形式；再对 ll 分类讨论，用矛盾解决空列表分支；在非空分支中展开 sllsll，解构存在量词和分离合取，为堆结论提供 hh、tt、qq 三个例证；最后简化纯事实，通过框架消除消去两侧共有的空间资源。

本节将依次完成这些步骤。首先要考虑的是：普通目标是否足以表达这种资源结构？

理解分离逻辑目标

普通目标将蕴含作为一个整体处理。前一节中的普通目标是 [Gamma ?- p][Gamma ?- p]。引入 unfold_sll_not_nullunfold_sll_not_null 的外层全称量词和蕴含后，得到：

（本页的目标框仅作示意。在策略的实际打印输出中，普通目标分为 Assumptions:Assumptions: 和 Conclusion:Conclusion: 两部分，分离逻辑目标分为 Assumptions:Assumptions:、Antecedents:Antecedents: 和 Consequent:Consequent: 三部分。自动引入的假设也标为 HH；这里写成 P_ptP_pt，以便与下文的堆前件 HH 区分。）这是一个普通目标：整条蕴含 sll pt l |-- ...sll pt l |-- ... 被当作一个 boolbool 结论处理。目标树只知道这是一个待证命题，并不了解蕴含的内部结构。证明器无法像操作普通假设那样按标签操作堆资源；对目标的任何变换都可能破坏蕴含的形态。

分离逻辑目标显式表示资源结构。下文使用如下记号：

p, q               : bool
H, K, P, Q         : hprop
Lambda             : 有序且带标签的普通逻辑前件
Delta              : 有序且带标签的堆前件
ant(Delta)         = Delta 中堆断言之分离合取
p, q               : bool
H, K, P, Q         : hprop
Lambda             : 有序且带标签的普通逻辑前件
Delta              : 有序且带标签的堆前件
ant(Delta)         = Delta 中堆断言之分离合取
定义 2（分离逻辑目标）。 分离逻辑目标写作 [Lambda; Delta ?- K][Lambda; Delta ?- K]，表示普通逻辑判断 |Lambda| ?- (ant(Delta) |-- K)|Lambda| ?- (ant(Delta) |-- K)。其中，LambdaLambda 保存普通逻辑前件，这些前件可以任意复制或丢弃；DeltaDelta 保存堆资源，每一项都在使用后消耗；KK 是保留为一个整体的堆结论。

打印时，两类前件分别显示在两个区域中：

回到链表引理，进入分离逻辑目标模式后得到：

现在，P_ptP_pt 是普通逻辑前件，可以用于重写和推导矛盾；HH 是堆资源，只能通过分离逻辑规则使用；堆结论则保留为一个整体。这一划分直接反映了分离逻辑证明的结构。

进入分离逻辑目标模式

从蕴含进入：SL_MODESL_MODE。

最稳妥的做法是先将整个前件命名为 "H""H"：

gnode_list gns = SL_MODE(gn, "H");
gnode_list gns = SL_MODE(gn, "H");

如果已知前件的结构，也可以在进入目标模式时一并解构。模式语言仅有五种构造：

模式 含义
HH 将整个堆前件命名为 HH
H_1 * H_2H_1 * H_2 拆分外层的分离合取
H_1 | H_2H_1 | H_2 拆分外层的析取，产生两条分支
x ? Hx ? H 消去外层的存在量词，以新变量 xx 开启
[L][L] 把该位置上的一条 fact(p)fact(p) 从堆中移入普通假设，记为 L: pL: p

解析器从括号中读取结构，不设运算符优先级，因此复杂模式必须显式加括号：

SL_MODE(g, "H_1 * ((x ? H_2) | H_3)");
SL_MODE(g, "H_1 * ((x ? H_2) | H_3)");

从堆断言等式进入：EQ_SLTACEQ_SLTAC。另一种常见目标是两个堆断言相等。此时 SL_MODESL_MODE 不适用，应改用反对称性将等式拆分为两个有向蕴含。

两条分支各自有独立的标签命名空间，因此 L_1L_1 和 L_2L_2 可以使用同一名称。

分析堆前件

进入分离逻辑目标模式后，证明器首先要处理 DeltaDelta 中已有的资源。堆资源与普通逻辑前件的根本区别在于线性：每个资源恰好使用一次，既不能随意复制，也不能随意丢弃。

解构外层结构。对单个带标签的堆前件，最常用的原子策略如下：

前件形态 策略 效果
L:(P ** Q)L:(P ** Q) HANT_SEP_SLTACHANT_SEP_SLTAC 拆分为两个带标签的资源
L:(P || Q)L:(P || Q) HANT_DISJ_SLTACHANT_DISJ_SLTAC 每个析取支产生一个子目标
L:(exists x. H)L:(exists x. H) HANT_EXISTS_SLTACHANT_EXISTS_SLTAC 以新变量开启存在量词
L:HL:H HANT_RENAME_SLTACHANT_RENAME_SLTAC 仅更改标签，不更改内容

这些策略都保留堆结论。例如，拆分分离合取可以抽象地表示为：

     [Lambda; Delta_R,L_1:P,L_2:Q ?- K]
------------------------------------------------
          [Lambda; Delta,L:(P ** Q) ?- K]
     [Lambda; Delta_R,L_1:P,L_2:Q ?- K]
------------------------------------------------
          [Lambda; Delta,L:(P ** Q) ?- K]

分离合取产生一个子目标（两种资源同时存在）；析取产生两个子目标（状态可能满足任一侧）；开启存在量词时，必须选取一个不会捕获目标中自由变量的新名称。

递归解构整个前件：

gnode_list HANT_DESTRUCT_SLTAC(
  const gnode gn, const char *L, const char *pattern);
gnode_list AUTO_HANT_DESTRUCT_SLTAC(const gnode gn);
gnode_list HANT_DESTRUCT_SLTAC(
  const gnode gn, const char *L, const char *pattern);
gnode_list AUTO_HANT_DESTRUCT_SLTAC(const gnode gn);

前者按给定模式解构；后者按顺序遍历上下文，递归拆分每个可见的 ****、|||| 和 existsexists，并在每个新产生的析取分支上继续，直到不再有这类外层结构。

将纯事实移到普通逻辑区域。要让 fact(p)fact(p) 参与普通逻辑重写、算术推理或矛盾推导，需要将它从堆区域移入 LambdaLambda：

gnode INTRO_FACT_SLTAC(
  const gnode gn, const const_cstr_list lbs);
gnode AUTO_INTRO_FACT_SLTAC(const gnode gn);
gnode INTRO_FACT_SLTAC(
  const gnode gn, const const_cstr_list lbs);
gnode AUTO_INTRO_FACT_SLTAC(const gnode gn);

INTRO_FACT_SLTACINTRO_FACT_SLTAC 按指定标签选取纯事实；自动版则选取当前堆前件中所有顶层的 fact(p)fact(p)。移入后，这些命题就可以像前一节的普通假设一样使用。

重写、魔术棒与矛盾分支的处理。另外还有三种常见操作：

  • HANT_CONV_SLTACHANT_CONV_SLTAC：以变换重写指定堆前件；
  • WAND_MP_SLTACWAND_MP_SLTAC：从 (P -* Q)(P -* Q) 和资源 PP 产生资源 QQ；
  • CONTR_SLTACCONTR_SLTAC：当某个堆前件规范化为 fact(false)fact(false) 时解决该分支。

例如，在链表例子的空列表分支中，展开 sll pt []sll pt [] 得到 fact(pt == 0i)fact(pt == 0i)。用普通逻辑前件 ~(pt == 0i)~(pt == 0i) 重写后，资源变为矛盾，CONTR_SLTACCONTR_SLTAC 随即解决该分支。

构造堆结论

分析堆前件回答的是“已有些什么”；操作堆结论回答的是“还需要构造什么”。结论 KK 保留为一个整体，使用什么策略取决于它的最外层结构。

分离合取划分资源。如果目标是 K_1 ** K_2K_1 ** K_2，两个子目标不能像普通逻辑合取那样各自继承全部资源。证明者必须指明哪些前件资源分配给左侧子目标，其余的则分配给右侧：

析取、存在量词与纯事实。其余用于堆结论的策略也可以按结论的结构分类：

结论形态 策略 证明者的选择
K_1 || K_2K_1 || K_2 DISJ1_SLTACDISJ1_SLTAC / DISJ2_SLTACDISJ2_SLTAC 选择左或右析取支
exists x. Hexists x. H EXISTS_SLTACEXISTS_SLTAC 提供例证
多个外层 existsexists LIST_EXISTS_SLTACLIST_EXISTS_SLTAC 按顺序提供例证列表
P ** (exists x. Q)P ** (exists x. Q) EXISTS_PULL_SLTACEXISTS_PULL_SLTAC 先将存在量词提至最外层
若干 fact(p)fact(p) PURE_SLTACPURE_SLTAC 将纯事实分离为一个普通目标，保留其余部分
KK HCON_CONV_SLTACHCON_CONV_SLTAC 以变换重写整个堆结论

例如：

     [Lambda; Delta ?- H[w/x]]
-------------------------------- EXISTS_SLTAC w
 [Lambda; Delta ?- exists x. H]
     [Lambda; Delta ?- H[w/x]]
-------------------------------- EXISTS_SLTAC w
 [Lambda; Delta ?- exists x. H]

其中例证的类型必须与存在量词变量的类型一致。

规范化、清理与框架消除

许多分离逻辑目标在语义上已经成立，只是两侧的语法形式有所不同：可能只有一侧展开了定义，可能还有纯事实尚未简化，也可能 **** 的结合方式或排列顺序不同。这类目标需要先规范化，再消去共同资源。

变换与清理。

gnode CONV_SLTAC(const gnode gn, const conv cv);
gnode CONV_WITH_ASMP_SLTAC(
  const gnode gn,
  conv (*cvf)(thm_list),
  const thm_list ths);
gnode CLEAN_SLTAC(const gnode gn);
void EMP_SLTAC(const gnode gn);
gnode CONV_SLTAC(const gnode gn, const conv cv);
gnode CONV_WITH_ASMP_SLTAC(
  const gnode gn,
  conv (*cvf)(thm_list),
  const thm_list ths);
gnode CLEAN_SLTAC(const gnode gn);
void EMP_SLTAC(const gnode gn);

CONV_SLTACCONV_SLTAC 依次重写堆结论和每个堆前件。CONV_WITH_ASMP_SLTACCONV_WITH_ASMP_SLTAC 额外将 LambdaLambda 中的普通逻辑前件作为假设定理传递给变换函数，适合“按定义展开再根据当前分支事实简化”的场景。CLEAN_SLTACCLEAN_SLTAC 删除 empemp、fact(true)fact(true) 等单位元并规范化其余部分。如果规范化后堆结论为 empemp 且每个堆前件都是 empemp 或平凡为真的事实，EMP_SLTACEMP_SLTAC 解决该目标。

框架消除。除 EMP_SLTACEMP_SLTAC 外，最常见的收尾方式是消去两侧的共同资源：

gnode FRAME_SLTAC(
  const gnode gn, const const_cstr_list labels);
gnode AUTO_FRAME_SLTAC(const gnode gn);
gnode FRAME_SLTAC(
  const gnode gn, const const_cstr_list labels);
gnode AUTO_FRAME_SLTAC(const gnode gn);

FRAME_SLTACFRAME_SLTAC 按标签选择堆前件，在堆结论的顶层多重集中找到与之相等的资源，再将两者同时消去（不解决目标）；AUTO_FRAME_SLTACAUTO_FRAME_SLTAC 按前件顺序贪心地消去所有可匹配的资源，然后清理单位元，如果目标已变得平凡，就将其解决。

框架匹配按出现次数进行。如果前件中某个资源有两个副本而结论中只有一个，同一结论资源不能被匹配两次。堆资源按多重集处理，普通逻辑假设按集合处理，两者的关键区别就在这里。

自动初始化：AUTO_INIT_SLTACAUTO_INIT_SLTAC

进入分离逻辑目标模式、解构堆前件、清理单位元、引入纯事实、尝试框架消除，这些都是机械性步骤，也常常以相同顺序出现在证明的开头。因此，库将它们封装为一个组合策略。

定义 3（组合策略）。 组合策略依次调用已有策略，将每一步尚未求解的叶节点传给下一步。它不引入新的推理规则；健全性来自它所组合的原子策略。

这组步骤首先引入普通逻辑量词和前件，然后进入分离逻辑目标模式；接着解构可见的堆前件、清理平凡资源、将顶层的纯事实移到普通逻辑区域，最后尝试消去可直接匹配的框架资源。由于拆分析取可能产生分支，它返回当前所有尚未求解的叶节点，而非单个 gnodegnode。

完整的链表证明

现在，证明所需的原子策略都已介绍完毕，我们也知道了 AUTO_INIT_SLTACAUTO_INIT_SLTAC 在开头组合了哪些步骤。回到开篇的链表引理，可以将这些工具串联起来：

PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode gn = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(gn, `l:(int)list`, "P_l");
  gn = gns[0];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(gn, "H");
  gn = gns[1];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  gn = AUTO_HANT_DESTRUCT_SLTAC(gn)[0];
  gn = LIST_EXISTS_SLTAC(
    gn, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  gn = CONV_SLTAC(gn, simp_conv(thm_list_n(0)));
  gn = AUTO_FRAME_SLTAC(gn);
  return gnode_prove(root);
}
PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode gn = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(gn, `l:(int)list`, "P_l");
  gn = gns[0];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(gn, "H");
  gn = gns[1];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  gn = AUTO_HANT_DESTRUCT_SLTAC(gn)[0];
  gn = LIST_EXISTS_SLTAC(
    gn, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  gn = CONV_SLTAC(gn, simp_conv(thm_list_n(0)));
  gn = AUTO_FRAME_SLTAC(gn);
  return gnode_prove(root);
}

初始化：让目标显式表示资源。 AUTO_INIT_SLTACAUTO_INIT_SLTAC 引入外层量词和前件，并将目标转为显式表示资源的形式；运行后只剩一个尚未求解的叶节点，因此示例取返回列表的第一个元素。

对逻辑列表进行分类讨论。 CASES_TAC(gn, CASES_TAC(gn, l:(int)list, "P_l"), "P_l") 只改变普通逻辑前件，因此两个子目标均停留在分离逻辑目标模式中。空列表分支获得 l = []l = []；非空分支获得 l = a0 :: a1l = a0 :: a1。

空列表分支：展开后得到矛盾。用 sll_defsll_def 展开 sll pt []sll pt []，再用当前分支的逻辑前件化简。此时资源 HH 变为矛盾，CONTR_SLTACCONTR_SLTAC 便可解决该分支。

非空分支：展开、提供例证、框架消除。展开定义后，可以看到指针非空的事实、头字段和尾字段，以及后继链表的 sllsll 资源。AUTO_HANT_DESTRUCT_SLTACAUTO_HANT_DESTRUCT_SLTAC 将外层的 **** 和 existsexists 转化为各自带标签的独立资源。分类讨论和展开已经确定了三个例证，LIST_EXISTS_SLTACLIST_EXISTS_SLTAC 将它们一并提供；CONV_SLTACCONV_SLTAC 简化纯事实 l == a0 :: a1l == a0 :: a1；两侧剩余的空间资源逐项匹配，AUTO_FRAME_SLTACAUTO_FRAME_SLTAC 将它们逐一消去，解决目标。

最后调用 gnode_prove(root)gnode_prove(root)。此时树中的每个叶节点都已求解，因此可以自底向上重建证明，返回原始引理对应的定理。

用户自定义组合策略

AUTO_INIT_SLTACAUTO_INIT_SLTAC 展示了库如何封装一套稳定的机械性流程。用户也可以用同样的方式组合已有策略，为自己的证明构建作用范围更小、更有针对性的自动步骤。

如果每一步都产生单个子目标，可以直接串联：

gnode MY_CLEAN_FRAME_SLTAC(const gnode gn) {
  gnode next_gn = CLEAN_SLTAC(gn);
  next_gn = AUTO_INTRO_FACT_SLTAC(next_gn);
  next_gn = AUTO_FRAME_SLTAC(next_gn);
  return next_gn;
}
gnode MY_CLEAN_FRAME_SLTAC(const gnode gn) {
  gnode next_gn = CLEAN_SLTAC(gn);
  next_gn = AUTO_INTRO_FACT_SLTAC(next_gn);
  next_gn = AUTO_FRAME_SLTAC(next_gn);
  return next_gn;
}

但处理析取或分离合取结论的策略可能产生分支。此时，必须对当前所有叶节点应用下一步策略：

gnode_list gns = AUTO_HANT_DESTRUCT_SLTAC(gn);
APPLY_ALL_TAC(CLEAN_SLTAC, gns);
gns = gnode_leaves(gn);
gnode_list gns = AUTO_HANT_DESTRUCT_SLTAC(gn);
APPLY_ALL_TAC(CLEAN_SLTAC, gns);
gns = gnode_leaves(gn);

这里需要重新调用 gnode_leavesgnode_leaves 获取叶节点：上一步可能已经解决了某些目标，或产生了新分支，因此旧列表未必还对应子树中尚未完成的证明工作。

分离逻辑策略何以健全

前一节已经介绍了通用的健全性机制：当策略展开一个目标时，它必须记录一个验证函数；子目标得到证明后，验证函数重建上层定理，gnode_provegnode_prove 将整棵树归约到根定理。分离逻辑策略复用同一机制。

分离逻辑目标 [Lambda; Delta ?- K][Lambda; Delta ?- K] 只是将命题 |Lambda| ?- (ant(Delta) |-- K)|Lambda| ?- (ant(Delta) |-- K) 的结构显式表示出来。当策略更改标签、拆分前件或选定结论时，其验证函数调用 proof_slproof_sl 中已经证明的前向规则来恢复原始蕴含。例如，框架消除在子目标中临时移除了共同资源，验证函数则用框架规则重建上层目标。

需要额外保证的是资源线性：普通逻辑前件按集合检查，堆前件则按多重集检查，计入每个资源的出现次数。同一资源不能被消耗两次。当标签、资源计数、变量新鲜性或类型不满足策略要求时，策略直接失败；它不会将尚未满足的条件当作事实。

小结

  • 普通目标将 H |-- KH |-- K 整体当作一个命题；分离逻辑目标则将普通逻辑前件、带标签的堆前件和堆结论分开保存，直接反映资源结构。
  • SL_MODESL_MODE 处理分离逻辑蕴含；EQ_SLTACEQ_SLTAC 通过两条有向蕴含处理堆断言等式。
  • HANT_*_SLTACHANT_*_SLTAC 分析已有资源；INTRO_FACT_SLTACINTRO_FACT_SLTAC 将纯事实移入普通逻辑区域；SEP_SLTACSEP_SLTAC 及析取/存在量词策略构造堆结论。
  • 变换与清理是统一的；FRAME_SLTACFRAME_SLTAC 和 AUTO_FRAME_SLTACAUTO_FRAME_SLTAC 按出现次数消去共同资源。
  • AUTO_INIT_SLTACAUTO_INIT_SLTAC 这样的组合策略适合处理机械性步骤；分支、例证和资源划分通常需要证明者显式输入。
  • 分离逻辑策略仍通过目标树验证函数重建定理，最终由 HOL 内核检查。

链表例子展示了一套典型的证明步骤：初始化目标，对纯数据分类讨论，展开空间谓词，提供例证，规范化两侧，再通过框架消除消去共同资源。后续对更复杂的数据结构进行证明时，也会沿用这条主线。