C*：开发与证明一体化

操作的声明与应用

EN | 中文

上一节末尾用一行操作式代码展开了链表节点，当时直接使用了现成的操作。本节说明这个工具从何而来：如何将一条健全的局部资源变换封装为操作（operation），用消耗/产出模式描述它，并在声明时卸除证明义务；应用操作时，又如何得到并提交一条完整状态定理。本节以已通过验证的 tutorial/10_reverse_op.ctutorial/10_reverse_op.c 为例。这个程序实现链表的原地反转，其中的每一次视图转换都用操作或通用状态变换函数表达。

操作消除的重复工作

上一节示例中的展开引理只需证明一次，此后便可反复使用；但应用引理所需的辅助工作仍要重复。在每个需要展开链表节点的程序点，用户都要完成以下步骤：

  • 用当前指针和列表（v_vv_v、l2l2）实例化引理参数；
  • 选中正确的资源——是 sll v_v l2sll v_v l2，而不是旁边的 sll w_v l1sll w_v l1；
  • 根据分支中的事实卸除前提 ~(v_v == 0i)~(v_v == 0i)；
  • 为展开产生的存在变量确定稳定的名称；
  • 把其余资源作为框架保留，并提交完整状态蕴含——若状态有多个分支，还须逐分支处理。

前向证明一节曾为一个程序点手写这套辅助代码。如果有十处需要展开，就要写十份这样的代码；引理的陈述一旦调整，这十处也都要修改。

定义 1（操作）。 操作是一条局部资源变换的参数化协议：将一条已证明的引理、参数的实例化方式，以及从当前状态选择待消耗资源的方式封装在一起。声明一个操作，就是写出它的模式（schema）；应用一个操作，则由证明库自动完成选择、实例化、提升与提交。

声明一个操作

五个组成部分

一份操作模式可以概括为：

O = (name, inputs, consumes, facts, produce)
O = (name, inputs, consumes, facts, produce)
部分 回答的问题 展开非空链表时
namename 用什么名称绑定操作、报告诊断信息？ unfold_sll_not_nullunfold_sll_not_null
inputsinputs 调用者提供什么？ ptpt
consumesconsumes 选择哪些资源？ sll pt lsll pt l
factsfacts 需要哪些纯前提？ ~(pt == 0i)~(pt == 0i)
produceproduce 选中的资源变成什么？ exists h t q. ...exists h t q. ...

inputsinputs 与其余部分各有分工：调用者只提供自己已经知道的稳定参数（这里是一个地址）；资源内部的未知数据，如逻辑列表和后继指针，则通过匹配从当前状态中取得。

一份实际的声明

操作用 decl_operationdecl_operation 声明。声明之前，须先定义一个证明回调，其名称为操作名加上 _proof_proof 后缀。下面是本部分一直使用的展开操作，与 10_reverse_op.c10_reverse_op.c 中的声明一致。回调使用后向分离逻辑策略，直接完成该模式所要求的证明：

PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode g = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(g, `l:(int)list`, "P_l");
  g = gns[0];                       // l == []：与 ~(pt == 0i) 矛盾
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(g, "H");
  g = gns[1];                       // l == a0 :: a1：展开并逐项匹配
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  g = AUTO_HANT_DESTRUCT_SLTAC(g)[0];
  g = LIST_EXISTS_SLTAC(g, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  g = CONV_SLTAC(g, simp_conv(thm_list_n(0)));
  g = AUTO_FRAME_SLTAC(g);
  return gnode_prove(root);
}
decl_operation(unfold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(1, `sll (KEY pt) (CAPTURE l)`),
  term_list_n(1, `~(pt == 0i)`),
  `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`
)
PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode g = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(g, `l:(int)list`, "P_l");
  g = gns[0];                       // l == []：与 ~(pt == 0i) 矛盾
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(g, "H");
  g = gns[1];                       // l == a0 :: a1：展开并逐项匹配
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  g = AUTO_HANT_DESTRUCT_SLTAC(g)[0];
  g = LIST_EXISTS_SLTAC(g, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  g = CONV_SLTAC(g, simp_conv(thm_list_n(0)));
  g = AUTO_FRAME_SLTAC(g);
  return gnode_prove(root);
}
decl_operation(unfold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(1, `sll (KEY pt) (CAPTURE l)`),
  term_list_n(1, `~(pt == 0i)`),
  `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`
)

这份模式从上到下依次指定：操作名为 unfold_sll_not_nullunfold_sll_not_null；调用者提供地址 ptpt；消耗一个资源——位于 ptpt 处的 sllsll，其逻辑列表被捕获为 ll；应用前须满足纯前提 ~(pt == 0i)~(pt == 0i)；选中的资源变为结构分解事实 l == h :: tl == h :: t、两个字段单元和尾部链表。回调证明的义务本质上就是分离逻辑的后向证明中的展开引理，在声明时证明一次，此后在任何使用点都无须重新证明。

健全性目标

KEYKEY、CAPTURECAPTURE、DEFERDEFER 在逻辑中都是恒等函数，只对匹配过程有意义。构造健全性目标时，证明库先擦除它们：

erase(CAPTURE t) = erase(KEY t) = erase(DEFER t) = t
erase(CAPTURE t) = erase(KEY t) = erase(DEFER t) = t

设 consumesconsumes 为 ，factsfacts 为 ，produceproduce 为 ，生成的目标为：

forall FV.
  f1 ==> ... ==> fn ==>
    (erase(c1) ** ... ** erase(cm) |-- Q)
forall FV.
  f1 ==> ... ==> fn ==>
    (erase(c1) ** ... ** erase(cm) |-- Q)

其中，所有自由模式变量都由全称量词绑定。接口不保证量词顺序。回调因此通过 goal_tmgoal_tm 接收目标，并应证明收到的项，不能自行重建一个看起来相同的目标。

decl_operationdecl_operation 展开为一次 operation_newoperation_new 调用：它检查模式的合法性，以生成的目标为参数调用一次证明回调，再检查返回的定理。该定理不得携带未卸除的假设，结论必须与目标 α-等价。

命题 2（声明不引入未经证明的变换）。 只有模式检查与证明回调检查都通过，得到的操作才携带其封闭引理。证明失败、返回带假设的定理，或证明了错误的陈述，都会使声明失败；不存在公理或未经检查的后备路径。

最简单的模式

折叠空链表既不需要输入参数，也不需要纯前提：

decl_operation(fold_sll_null,
  term_list_n(0),
  term_list_n(1, `emp`),
  term_list_n(0),
  `sll 0i []`
)
decl_operation(fold_sll_null,
  term_list_n(0),
  term_list_n(1, `emp`),
  term_list_n(0),
  `sll 0i []`
)

它表达局部资源变换 emp |-- sll 0i []emp |-- sll 0i []。初次了解操作值时，可以用这个简单例子观察其中的 inputsinputs / consumesconsumes / factsfacts / produceproduce 字段和 lemma=<proved>lemma=<proved> 标记。

消耗模式：KEYKEY、CAPTURECAPTURE、DEFERDEFER

consumesconsumes 中的每一项有两种作用：既是引理前件中的一个合取项，也是描述如何在分支中找到对应资源的匹配模式。匹配从左到右进行，使用三种标记。

KEYKEY：用可证明的等式定位资源

假设分支中同时存在

sll w_v l1 ** sll v_v l2
sll w_v l1 ** sll v_v l2

而操作以 pt := v_vpt := v_v 调用。模式 sll (KEY pt) (CAPTURE l)sll (KEY pt) (CAPTURE l) 先尝试第一个候选 sll w_v l1sll w_v l1：这要求证明 v_v = w_vv_v = w_v。由于无法证明这个等式，该候选被排除。再尝试第二个候选时，v_v = v_vv_v = v_v 成立，于是选中 sll v_v l2sll v_v l2。

KEY tKEY t 通过可证明的等式匹配资源，而非比较字符串。证明库按以下顺序尝试建立等式：精确相等；两边都是整数时使用整数算术；最后是通过 set_normalization_rulesset_normalization_rules 配置的规范化规则。 KEYKEY 只筛选候选，并不保证唯一性；若多个资源都满足模式，选中的仍是最前面的那个。模式因此应以稳定的语义身份作为键：地址、端点、所有者。

CAPTURECAPTURE：从状态中取得未知量

选中 sll v_v l2sll v_v l2 之后，CAPTURE lCAPTURE l 产生绑定 l := l2l := l2。 CAPTURE xCAPTURE x 必须引入一个尚未绑定的模式变量；每个变量至多捕获一次，之后的消耗项可以直接使用它，或在 KEYKEY、DEFERDEFER 中引用它。捕获读取的是状态中已经存在的逻辑值，不会凭空引入例证。

DEFERDEFER：推迟等式检查

设 pp 与 vv 都已绑定，模式

data_at (KEY p) Tint (DEFER v)
data_at (KEY p) Tint (DEFER v)

与 data_at p Tint ndata_at p Tint n 匹配时，先由 KEY pKEY p 定位资源；DEFER vDEFER v 只检查 vv 与 nn 的类型相容，并记录待处理的等式 v = nv = n。只有当所有消耗项都选择成功之后，证明库才尝试证明这些推迟的等式：先检查是否精确相等，再用 solve_eqsolve_eq 求解；仍无法证明的等式会登记为待证条件。

三种标记对照

标记 选择阶段 主要用途
KEY tKEY t 必须证明与候选相等 按语义身份筛选资源
CAPTURE xCAPTURE x 把候选子项绑定给新变量 取得未知的逻辑数据或抽象模型
DEFER tDEFER t 只要求类型相容 选择后再证明等式，必要时留下待证条件

普通变量也可以出现在模式中，但必须已经由输入参数或此前的捕获绑定；匹配时，只接受与其绑定值精确相等的项。

消耗项之间的依赖顺序

折叠一个非空节点需要三个资源，后面的模式使用前面的捕获结果：

decl_operation(fold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(3,
    `data_at (field_addr (KEY pt) Tlist Fhead) Tint (CAPTURE h)`,
    `data_at (field_addr (KEY pt) Tlist Ftail) Tptr (CAPTURE q)`,
    `sll (KEY q) (CAPTURE t)`
  ),
  term_list_n(1, `~(pt == 0i)`),
  `sll pt (h :: t)`
)
decl_operation(fold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(3,
    `data_at (field_addr (KEY pt) Tlist Fhead) Tint (CAPTURE h)`,
    `data_at (field_addr (KEY pt) Tlist Ftail) Tptr (CAPTURE q)`,
    `sll (KEY q) (CAPTURE t)`
  ),
  term_list_n(1, `~(pt == 0i)`),
  `sll pt (h :: t)`
)

匹配依次进行：以 ptpt 为键选中头字段，捕获头元素 hh；以 ptpt 为键选中尾字段，捕获该单元的当前值 qq；再以刚捕获的 qq 为键选中后继链表，捕获其内容 tt；产出 sll pt (h :: t)sll pt (h :: t)。它的证明回调与之前作用相同，只是这次证明的是列表引理的折叠方向。

每个消耗项都从尚未使用的顶层合取项中选择第一个匹配的资源；一旦选定，就不会重新选择：

consume_1 选中第一个匹配的资源
    |
consume_2 在剩余资源中继续选择
    |
后续失败不会让 consume_1 回头改选其他候选
consume_1 选中第一个匹配的资源
    |
consume_2 在剩余资源中继续选择
    |
后续失败不会让 consume_1 回头改选其他候选

这种确定性的贪心策略使匹配行为可以预测，也要求模式使用足以区分候选资源的 KEYKEY。

声明时检查什么

理解这三种匹配标记后，就可以列出 operation_newoperation_new 在声明时的全部检查：

  1. inputsinputs 中每一项都是 HOL 变量，并且彼此不同；
  2. 从左到右扫描 consumesconsumes：CAPTURE xCAPTURE x 必须引入新变量；普通变量以及 KEYKEY、DEFERDEFER 参数中的自由变量必须已经绑定；模式中不支持 λ-抽象；
  3. consumesconsumes、factsfacts、produceproduce 中的每个自由变量都来自输入参数或捕获；
  4. 证明回调返回不带假设、结论与生成目标 α-等价的定理。

声明时还没有具体的符号状态，因此不会检查某个程序点是否持有所需资源、某个分支是否满足所需事实；这些检查在应用阶段完成。

应用一个操作

两个状态接口

PROOF void apply_operation_st(
    const operation op, const term_list arguments);
PROOF void apply_operation_named_st(
    const operation op, const term_list arguments,
    const term_list existential_names);
PROOF void apply_operation_st(
    const operation op, const term_list arguments);
PROOF void apply_operation_named_st(
    const operation op, const term_list arguments,
    const term_list existential_names);

apply_operation_stapply_operation_st 把操作应用到当前状态的每一个分支。 apply_operation_named_stapply_operation_named_st 执行相同的变换，并按位置重命名产出断言最外层的存在量词前缀。

一次应用的完整过程

对每个分支，应用接口依次完成：

  1. 按位置把 argumentsarguments 绑定到 inputsinputs，检查数量与类型；
  2. 为输入参数以外的模式变量选择不与该分支冲突的新名称，避免名为 ll 的模式变量与状态中的同名变量冲突；
  3. 按 consumesconsumes 的顺序，从左到右在尚未使用的顶层合取项中贪心选择资源，并收集捕获结果；
  4. 用 solve_eqsolve_eq 处理各 DEFERDEFER 等式，使模式与实际资源对齐；
  5. 用输入参数与捕获结果实例化操作携带的封闭引理；
  6. 根据该分支的顶层事实，先用命题推理、再用整数算术证明 factsfacts 中的纯前提，并将其卸除；
  7. 用 local_applylocal_apply 提升得到的局部蕴含：未选中的资源作为框架保留，外层存在量词保持不变；
  8. 把各分支的定理合并为一条完整状态蕴含，在所有分支都成功之后，只调用一次 set_symbolic_stateset_symbolic_state 提交。

不同分支可以捕获不同的具体值、产生不同的后置状态，但操作必须能应用于每一个分支。

命题 3（从局部健全性到完整状态健全性）。 操作携带的引理证明从 consumesconsumes 到 produceproduce 的局部变换；框架规则保留每个分支中未参与的资源；析取单调性合并各分支。最终提交的是一条封闭的完整状态蕴含，不会绕过证明直接修改符号状态。

重命名只改变名称

PROOF apply_operation_named_st(
    unfold_sll_not_null,
    TERM_LIST(`v_v:addr`),
    TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));
PROOF apply_operation_named_st(
    unfold_sll_not_null,
    TERM_LIST(`v_v:addr`),
    TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));

这里 v_vv_v 是用于实例化输入参数 ptpt 的实参，而 hdhd、tltl、nxtnxt 只是产出断言最外层三个存在变量的名称。它们的值来自操作产生的存在量词，并非用户提供的例证。名称向量的长度必须等于产出断言最外层存在量词绑定子的数量，各名称的类型须与相应绑定子的类型一致。各名称还须彼此不同，且不得捕获产出体中的自由变量；所有分支使用同一个名称向量。这些名称需要保持稳定，因为随后的 assert_fact_stassert_fact_st、abbrev_stabbrev_st 等证明代码会直接引用它们。证明块可以直接使用这些名称，但由编译器在 C 作用域中处理的标注不能直接使用，例如后续调用上的 [[cst::where]][[cst::where]] 或内层循环的不变式。使用这些标注前，需要先用 [[cst::given(`hd:int`, `nxt:addr`)]];[[cst::given(`hd:int`, `nxt:addr`)]]; 从当前状态中绑定这些名称，做法见函数契约、循环不变式与断言。

操作式写法的反转循环

以下是已验证的 10_reverse_op.c10_reverse_op.c 中的完整函数（其中三个操作已在上文声明；另一个操作 unfold_sll_nullunfold_sll_null 与 fold_sll_nullfold_sll_null 对称，在前提 pt == 0ipt == 0i 下把 sll pt lsll pt l 转换为 fact(l == [])fact(l == [])）：

PROOF void forget_facts_st(term_list facts) {
  for (int i = 0; i < vector_size(facts); i++) {
    forget_fact_st(facts[i]);
  }
}
struct list *reverse(struct list *pt)
  PARAM(`l:(int)list`)
  REQUIRE(`sll pt l`)
  ENSURE(`sll __return (REVERSE l)`)
{
  PROOF set_default_types(TERM_LIST(
    `l:(int)list`, `l1:(int)list`, `l2:(int)list`,
    `w_v:int`, `v_v:int`, `pt__pre:int`
  ));
  struct list *w, *v;
  w = (void *)0;
  PROOF {
    // 产出已反转的前缀链表 `l1`（初始为 `[]`），
    // 由 `w_v`（初始为 NULL）指向
    apply_operation_st(fold_sll_null, NULL);
    abbrev_st(`w_v = 0i`);
    abbrev_st(`l1 = []`);
  }
  v = pt;
  PROOF {
    // 为尚未处理的后缀链表命名 `l2`（初始为 `l`），
    // 由 `v_v`（初始为 `pt__pre`）指向
    abbrev_occurrences_st(
      `v_v == pt__pre`,
      TERM_LIST(
        `data_at v__addr Tptr v_v`,
        `sll v_v l`
    ));
    abbrev_st(`l2 = l`);
    assert_fact_st(
      `l == (REVERSE l1) ++ l2`,
      simp_conv, THM_LIST(REVERSE_def, APPEND_def));
  }
  PROOF forget_facts_st(TERM_LIST(
    `l2 == l`, `v_v == pt__pre`, `l1 == []`, `w_v == 0i`
  ));
  PROOF term loop_inv = get_symbolic_state();
  while (v)
    INV(loop_inv)
  {
    PROOF apply_operation_named_st(
      unfold_sll_not_null,
      TERM_LIST(`v_v:addr`),
      TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));
    struct list *t = v->tail;
    v->tail = w;
    PROOF apply_operation_st(
      fold_sll_not_null,
      TERM_LIST(`v_v:addr`)
    );
    PROOF forget_fact_st(`~(v_v == 0i)`);
    PROOF {
      assert_fact_st(
        `l == (REVERSE (hd :: l1)) ++ tl:(int)list`, simp_conv,
        THM_LIST(REVERSE_def, APPEND_def, gsym_rule(APPEND_ASSOC)));
      rename_hexists_st("[l1'/l1] [l2'/l2]");
      abbrev_st(`l1 = hd :: l1':(int)list`);
      abbrev_st(`l2 = tl:(int)list`);
    }
    PROOF forget_facts_st(TERM_LIST(
      `l2 == tl`,
      `l1 == hd :: l1'`,
      `l == REVERSE l1' ++ l2'`,
      `l2' == hd :: l2`
    ));
    w = v;
    PROOF rename_locals_st();
    v = t;
    PROOF rename_locals_st();
    PROOF {
      substitute_st(sym_rule(assume_rule(`w_v == v_v'`)));
      substitute_st(sym_rule(assume_rule(`v_v == nxt`)));
      forget_facts_st(TERM_LIST(`w_v == v_v'`, `v_v == nxt`));
    }
  }
  PROOF apply_operation_st(unfold_sll_null, TERM_LIST(`v_v:addr`));
  PROOF assert_fact_st(`l1 == (REVERSE l):(int)list`, simp_conv,
    THM_LIST(APPEND_NIL, REVERSE_REVERSE)
  );
  PROOF substitute_st(assume_rule(`l1 == (REVERSE l):(int)list`));
  return w;
}
PROOF void forget_facts_st(term_list facts) {
  for (int i = 0; i < vector_size(facts); i++) {
    forget_fact_st(facts[i]);
  }
}
struct list *reverse(struct list *pt)
  PARAM(`l:(int)list`)
  REQUIRE(`sll pt l`)
  ENSURE(`sll __return (REVERSE l)`)
{
  PROOF set_default_types(TERM_LIST(
    `l:(int)list`, `l1:(int)list`, `l2:(int)list`,
    `w_v:int`, `v_v:int`, `pt__pre:int`
  ));
  struct list *w, *v;
  w = (void *)0;
  PROOF {
    // 产出已反转的前缀链表 `l1`（初始为 `[]`），
    // 由 `w_v`（初始为 NULL）指向
    apply_operation_st(fold_sll_null, NULL);
    abbrev_st(`w_v = 0i`);
    abbrev_st(`l1 = []`);
  }
  v = pt;
  PROOF {
    // 为尚未处理的后缀链表命名 `l2`（初始为 `l`），
    // 由 `v_v`（初始为 `pt__pre`）指向
    abbrev_occurrences_st(
      `v_v == pt__pre`,
      TERM_LIST(
        `data_at v__addr Tptr v_v`,
        `sll v_v l`
    ));
    abbrev_st(`l2 = l`);
    assert_fact_st(
      `l == (REVERSE l1) ++ l2`,
      simp_conv, THM_LIST(REVERSE_def, APPEND_def));
  }
  PROOF forget_facts_st(TERM_LIST(
    `l2 == l`, `v_v == pt__pre`, `l1 == []`, `w_v == 0i`
  ));
  PROOF term loop_inv = get_symbolic_state();
  while (v)
    INV(loop_inv)
  {
    PROOF apply_operation_named_st(
      unfold_sll_not_null,
      TERM_LIST(`v_v:addr`),
      TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));
    struct list *t = v->tail;
    v->tail = w;
    PROOF apply_operation_st(
      fold_sll_not_null,
      TERM_LIST(`v_v:addr`)
    );
    PROOF forget_fact_st(`~(v_v == 0i)`);
    PROOF {
      assert_fact_st(
        `l == (REVERSE (hd :: l1)) ++ tl:(int)list`, simp_conv,
        THM_LIST(REVERSE_def, APPEND_def, gsym_rule(APPEND_ASSOC)));
      rename_hexists_st("[l1'/l1] [l2'/l2]");
      abbrev_st(`l1 = hd :: l1':(int)list`);
      abbrev_st(`l2 = tl:(int)list`);
    }
    PROOF forget_facts_st(TERM_LIST(
      `l2 == tl`,
      `l1 == hd :: l1'`,
      `l == REVERSE l1' ++ l2'`,
      `l2' == hd :: l2`
    ));
    w = v;
    PROOF rename_locals_st();
    v = t;
    PROOF rename_locals_st();
    PROOF {
      substitute_st(sym_rule(assume_rule(`w_v == v_v'`)));
      substitute_st(sym_rule(assume_rule(`v_v == nxt`)));
      forget_facts_st(TERM_LIST(`w_v == v_v'`, `v_v == nxt`));
    }
  }
  PROOF apply_operation_st(unfold_sll_null, TERM_LIST(`v_v:addr`));
  PROOF assert_fact_st(`l1 == (REVERSE l):(int)list`, simp_conv,
    THM_LIST(APPEND_NIL, REVERSE_REVERSE)
  );
  PROOF substitute_st(assume_rule(`l1 == (REVERSE l):(int)list`));
  return w;
}

（set_default_typesset_default_types 为列出的变量名声明默认的 HOL 类型，此后的引用项可以省去大部分类型标注。）

初始化：构造不变式，再保存快照

入口处的两个证明块通过状态变换构造循环不变式，无须显式写出不变式。最简单的操作 fold_sll_nullfold_sll_null 把 empemp 变为空的已反转前缀 sll 0i []sll 0i []；几次 abbrev_stabbrev_st 与 abbrev_occurrences_stabbrev_occurrences_st 调用为相关值引入逻辑名称 w_vw_v、l1l1、v_vv_v、l2l2；assert_fact_stassert_fact_st 用化简证明模型等式 l == (REVERSE l1) ++ l2l == (REVERSE l1) ++ l2；forget_facts_stforget_facts_st 再清除引入名称时使用的临时定义等式。剩下的正是循环要维护的状态，于是代码直接保存快照：

PROOF term loop_inv = get_symbolic_state();
while (v)
  INV(loop_inv)
PROOF term loop_inv = get_symbolic_state();
while (v)
  INV(loop_inv)

循环体：展开、访问、折叠

进入循环体后，循环条件提供了 fact(~(v_v == 0i))fact(~(v_v == 0i))，因此可以应用 unfold_sll_not_nullunfold_sll_not_null。它通过 KEYKEY 排除 sll w_v l1sll w_v l1，选中 sll v_v l2sll v_v l2，再根据该事实卸除前提，展开当前节点，并将新的存在变量命名为 hdhd、tltl、nxtnxt。符号执行随即可以检查读取语句。 struct list *t = v->tail;struct list *t = v->tail; 之后，引擎报告：

旧的模型事实原样保留；展开只增加了结构分解事实 l2 == hd :: tll2 == hd :: tl。存储语句 v->tail = w;v->tail = w; 是真正的程序动作。执行后，尾单元变为 data_at (field_addr v_v Tlist Ftail) Tptr w_vdata_at (field_addr v_v Tlist Ftail) Tptr w_v，其余状态保持不变。

随后，fold_sll_not_nullfold_sll_not_null 消耗头单元和尾单元，并捕获尾单元的当前值 w_vw_v，再以这个值为键消耗 sll w_v l1sll w_v l1。它检查 ~(v_v == 0i)~(v_v == 0i)，产出 sll v_v (hd :: l1)sll v_v (hd :: l1)，同时将 sll nxt tlsll nxt tl 作为框架原样保留。尾单元的当前值决定了折叠时使用哪条链表，因此同一份折叠模式既适用于这个循环，也适用于 PSI 一节的访问器胶囊。

簿记：恢复不变式的形状

循环体的其余部分负责维护纯模型和名称，这些簿记工作全部由通用状态变换函数完成：

  • forget_fact_st(~(v_v == 0i))forget_fact_st(~(v_v == 0i)) 移除不变式并不携带的前提；
  • assert_fact_stassert_fact_st 用 REVERSEREVERSE/APPENDAPPEND 引理化简证明新的模型等式 l == (REVERSE (hd :: l1)) ++ tll == (REVERSE (hd :: l1)) ++ tl——这是嵌在操作式流程中的一个声明式步骤；
  • rename_hexists_st("[l1'/l1] [l2'/l2]")rename_hexists_st("[l1'/l1] [l2'/l2]") 将上一轮的列表改名，两个 abbrev_stabbrev_st 再用 l1 = hd :: l1'l1 = hd :: l1' 与 l2 = tll2 = tl 为新一轮的列表命名；forget_facts_stforget_facts_st 随后清除临时等式；
  • 每次游标赋值之后，rename_locals_strename_locals_st 重新为 C 变量的当前值命名：为单元的新值引入新的 w_vw_v 或 v_vv_v 绑定子，并将原绑定子改名为 v_v'v_v' 等历史名称；
  • 两个 substitute_stsubstitute_st 将其余资源中的历史名称替换为新的游标名称，最后一个 forget_facts_stforget_facts_st 清除改名等式。

w = v;w = v; 之后，引擎显示的资源已经具有不变式的形状，其中使用的是更新后的列表。sll v_v l1sll v_v l1 是加长后的前缀，sll nxt l2sll nxt l2 是缩短后的后缀：

游标与名称对齐之后，状态与保存的 loop_invloop_inv 匹配。这正是引擎在循环体末尾检查的那条蕴含。（块内局部变量 tt 的单元在代码块结束时由符号执行自动回收，不需要任何证明代码删除它。）

出口：后缀为空

循环退出时，分支已知 v_v == 0iv_v == 0i，unfold_sll_nullunfold_sll_null 把 sll v_v l2sll v_v l2 转换为 fact(l2 == [])fact(l2 == [])。 assert_fact_stassert_fact_st 随后由 l == REVERSE l1 ++ l2l == REVERSE l1 ++ l2、l2 == []l2 == [] 和 REVERSE_REVERSEREVERSE_REVERSE 证明 l1 == REVERSE ll1 == REVERSE l；substitute_stsubstitute_st 把 sll w_v l1sll w_v l1 改写为 sll w_v (REVERSE l)sll w_v (REVERSE l)，恰好是 return w;return w; 的后置条件。

示例 4（操作式与声明式各司其职）。 四个展开/折叠操作描述空间资源的转换，遵循可复用的协议，由当前状态计算后置状态。模型等式 l == (REVERSE (hd :: l1)) ++ tll == (REVERSE (hd :: l1)) ++ tl、l1 == REVERSE ll1 == REVERSE l 由用户陈述，交给 assert_fact_stassert_fact_st 证明。资源协议采用操作式写法，纯目标采用声明式写法，两种风格可以自由交错。

什么时候声明操作

如果一个资源动作在多个程序点反复出现，具有清晰且可证明的消耗/产出协议，需要从状态中捕获未知参数，并根据地址、端点、所有者等语义身份选择资源，那么它通常适合声明为操作。典型例子包括：数据结构节点的展开与折叠、数组片段的打开与关闭、抽象表示之间的转换、消耗线性令牌并产出其后继。

反过来，以下情形通常不需要新的操作：

  • 一次性的局部蕴含——直接用 apply_hconv_stapply_hconv_st 应用；
  • 全局的重写或代换——使用 rewrite_strewrite_st 及其同类接口；
  • 只为整理状态而做的一次性存在变量引入——abbrev_stabbrev_st；
  • 中间夹有 C 内存访问的多个资源阶段——它们永远不是一个操作。

常见失败与排查入口

现象 首先检查
声明失败 变量来源、消耗模式的结构，以及回调返回定理的假设与结论
实参数量或类型错误 argumentsarguments 是否与 inputsinputs 逐项对应？
找不到要消耗的资源 KEYKEY 是否足够明确？资源是否为尚未使用的顶层合取项？
匹配到非预期的资源 模式是否依赖了贪心选择的顺序，而实际需要添加一个按语义身份筛选的 KEYKEY？
出现待证条件 纯前提或 DEFERDEFER 等式为何无法自动证明？
重命名接口失败 名称的数量、类型、互异性与变量捕获
部分分支成功、整体失败 操作能否应用于每一个顶层分支？

排查时依次回答三个问题：模式本身是否合法、是否带有封闭证明？每个分支能否完成参数实例化、资源匹配和前提检查？所有分支能否保留框架、合并并一次提交？

小结

  • 操作将一条已证明的局部资源变换与参数实例化、资源选择方式封装在一起；inputsinputs 来自调用者，捕获值来自状态，factsfacts 陈述纯前提。
  • KEYKEY 用可证明的等式筛选资源，CAPTURECAPTURE 绑定未知量，DEFERDEFER 推迟等式检查；消耗项从左到右贪心选择，绝不回溯。
  • 声明阶段检查模式合法性，并要求证明回调给出封闭、α-等价的引理——没有未经证明的后备路径；资源匹配发生在应用阶段，逐分支进行，整个状态只提交一次。
  • 反转证明由四个操作加通用状态变换函数驱动，遵循“展开——程序访问——折叠——模型更新”的节奏；循环不变式也由同一批变换函数构造，再用 get_symbolic_stateget_symbolic_state 保存为快照。