操作的声明与应用

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

设 consumes 为，facts 为，produce 为，生成的目标为：


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

最简单的模式

折叠空链表既没有 inputs，也没有纯前提：


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> 标记。

一个无须前提的变体

当每个使用点的契约都把链表写成 cons 形式——如 PSI 胶囊一节中前置条件 sll p (h :: t)sll p (h :: t) 那样——消耗模式就可以按形状匹配 cons，并嵌套捕获：


sll (KEY pt) ((CAPTURE h) :: (CAPTURE t))


sll (KEY pt) ((CAPTURE h) :: (CAPTURE t))

这样的展开完全不需要非空前提；相反，它会产出 fact(~(pt == 0i))fact(~(pt == 0i))，而这正是折叠操作随后要消耗的前提。下文的反转循环中，不变式以抽象列表 l2l2 指代后缀，因此上面这份带前提的模式才是合适的。

消耗模式：`KEYKEY`、`CAPTURECAPTURE`、`DEFERDEFER`

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

`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`	只要求类型相容	选择后再证明等式，必要时留下待证条件

普通变量也可以出现在模式中，但它必须已经绑定——来自 input 或更早的捕获——此后只与其绑定值精确匹配。

消耗项之间的依赖顺序

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


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 的声明检查：

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

声明时还不存在具体的符号状态，因此不会检查某个程序点是否真的持有所需资源、required facts 是否在某个分支中成立——这些属于应用阶段。

应用一个操作

两个状态接口


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 执行相同的变换，并按位置重命名产出断言最外层的存在量词前缀。

一次应用的完整过程

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

按位置把 argumentsarguments 绑定到 inputsinputs，检查数量与类型；
对照该分支刷新非 input 的模式变量——因此名为 ll 的模式变量绝不会与状态中恰好同名的变量冲突；
按 consumes 顺序在尚未使用的顶层合取项中从左到右贪心选择资源，积累捕获结果；
用 solve_eqsolve_eq 处理各 DEFERDEFER 等式，使模式与实际资源对齐；
用 inputs 与捕获结果实例化操作携带的封闭引理；
从该分支的顶层事实证明 facts 中的纯前提——先命题推理，再整数算术——并将其卸除；
用 local_applylocal_apply 提升得到的局部蕴含：未选中的资源作为框架保留，外层存在量词保持不变；
把各分支的定理合并为一条完整状态蕴含，在所有分支都成功之后，只调用一次 set_symbolic_stateset_symbolic_state 提交。

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

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

重命名只改变名称


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 是用于实例化 input ptpt 的实参，而 hdhd、tltl、nxtnxt 只是产出断言最外层三个存在变量的名称。它们的值来自操作产生的存在量词——并非用户提供的例证。名称向量必须与产出的绑定变量数量一致、类型逐项一致、彼此不同，且不得捕获产出体中的自由变量；所有分支使用同一个名称向量。名称的稳定性并非小事：随后的证明代码——某个 assert_fact_stassert_fact_st、某个 abbrev_stabbrev_st——将直接引用这些名字。

操作式写法的反转循环

以下是已验证的 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)

快照得到的循环不变式


exists w_v v_v l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll v_v l2 **
    sll w_v l1


exists w_v v_v l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll v_v l2 **
    sll w_v l1

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

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

struct list *t = v->tail;struct list *t = v->tail; 之后的符号状态


exists nxt hd tl w_v l1 l2 v_v.
    fact (~(v_v == 0i)) **
    fact (l == REVERSE l1 ++ l2) **
    fact (l2 == hd :: tl) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr nxt **
    sll nxt tl


exists nxt hd tl w_v l1 l2 v_v.
    fact (~(v_v == 0i)) **
    fact (l == REVERSE l1 ++ l2) **
    fact (l2 == hd :: tl) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr nxt **
    sll nxt tl

旧的模型事实原样保留；展开只增加了结构分解事实 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 是缩短后的后缀：

w = v;w = v; 之后的符号状态


exists w_v v_v nxt l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr v_v **
    data_at pt__addr Tptr pt__pre **
    sll nxt l2 **
    sll v_v l1


exists w_v v_v nxt l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr v_v **
    data_at pt__addr Tptr pt__pre **
    sll nxt l2 **
    sll v_v l1

游标与名称对齐之后，状态与保存的 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 证明。资源协议用操作式，纯目标用声明式：两种风格自由交错。

什么时候声明操作

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

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

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

常见失败与排查入口

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

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

小结

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