有证明的视图转换

在前向证明一节中，链表反转的循环在读取 v->tailv->tail 之前需要一个证明块：实例化展开引理，再用 local_applylocal_apply 把结果写入状态。但在这个程序点，符号状态已经包含 sll v_v l2sll v_v l2，也就是说，循环已经拥有整条剩余链表。究竟缺少什么？

这里并不缺少内存，缺少的是这块内存的一个视图（view）。在这个视图中，v->tailv->tail 对应的单元以符号执行引擎能够直接使用的资源形式出现：

data_at (field_addr v_v Tlist Ftail) Tptr nxt

data_at (field_addr v_v Tlist Ftail) Tptr nxt

符号状态描述了当前程序点所拥有的资源和已知的事实。即使具体内存完全没有变化，同一状态也可以由多个不同的分离逻辑断言描述。

引擎需要什么形态的视图，取决于下一步要检查的动作，而不只取决于我们如何理解算法。其中有两类常见的要求。

考虑反转循环中的两条核心语句：

struct list *t = v->tail;
v->tail = w;

struct list *t = v->tail;
v->tail = w;

要机械地检查这两条语句，当前视图必须显式呈现 v->tailv->tail 对应的单元：

data_at (field_addr v_v Tlist Ftail) Tptr nxt

data_at (field_addr v_v Tlist Ftail) Tptr nxt

这一个资源就提供了引擎所需的全部信息：我们拥有地址 field_addr v_v Tlist Ftailfield_addr v_v Tlist Ftail 处的单元，可以访问它；该单元按类型 TptrTptr 解释，读取会得到 nxtnxt；写入后，资源中表示值的部分会变为新写入的值。若状态中只有 sll v_v l2sll v_v l2，我们在逻辑上确实拥有这个单元，但它尚未以引擎能够用于本次访问的形式呈现出来。

假设被调用函数的前置条件是 P x ** Q yP x ** Q y，而调用方的资源目前折叠在另一个谓词 R x yR x y 之中。应用契约之前，需要先建立一条局部蕴含：

R x y |-- P x ** Q y

R x y |-- P x ** Q y

这条蕴含把所需资源表示为前置条件能够匹配的分离合取项。调用结束后，后置条件可能又需要折叠回调用方所维护的视图。因此，视图变化也是衔接模块化契约的基本步骤，并非只在字段访问时才需要。

回顾单向链表谓词：

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

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

这个定义同时承担三项工作：列出并封装组成链表的具体内存资源，用逻辑列表为功能正确性推理提供模型，以及建立折叠视图（folded view）与节点展开视图（exposed-node view）之间的逻辑联系。

当 ptpt 非空、链表内容为 h :: th :: t 时，折叠视图 sll pt (h :: t)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

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

两种视图没有哪一种“更真实”：折叠视图适合把整条链表作为一个逻辑对象使用，展开视图适合验证当前节点上的字段访问。它们只是为不同的推理步骤划定了不同的资源边界。

更新链表节点的字段时，各步骤按如下顺序进行：

折叠视图        sll pt (h :: t)
  |  视图转换：展开，由蕴含定理支撑
展开视图        两个字段的 data_at
  |  C 读取 / 存储，由符号执行处理
更新后的单元     尾单元已保存新值
  |  视图转换：折叠，由蕴含定理支撑
更新后的折叠视图  sll 已反映新的字段值

折叠视图        sll pt (h :: t)
  |  视图转换：展开，由蕴含定理支撑
展开视图        两个字段的 data_at
  |  C 读取 / 存储，由符号执行处理
更新后的单元     尾单元已保存新值
  |  视图转换：折叠，由蕴含定理支撑
更新后的折叠视图  sll 已反映新的字段值

证明时不必追求某一种规范写法，只需让视图符合当前正在检查的动作所需的形态。

这里只需要证明代码与符号状态之间的一个接口：

PROOF {
  term st = get_symbolic_state();
  thm vs_thm = /* 证明  |- st |-- st'  */;
  set_symbolic_state(vs_thm);
}

PROOF {
  term st = get_symbolic_state();
  thm vs_thm = /* 证明  |- st |-- st'  */;
  set_symbolic_state(vs_thm);
}

get_symbolic_state()get_symbolic_state() 以 termterm 的形式返回当前完整状态 。证明代码可以检查它，并计算出候选的新视图 ，但仅有这个候选项还不够。 set_symbolic_stateset_symbolic_state 只接受一条封闭的完整状态蕴含定理

|- S |-- S'

|- S |-- S'

只有当其前件与当前状态在分离合取的交换、结合与单位元（ACU）意义下匹配时，后件才会成为新的当前状态。

两种风格最终都要得到同一形式的定理，区别在于目标视图从哪里来。

我们在同一个程序点上比较两种写法：在反转循环读取 v->tailv->tail 之前展开当前节点。循环把链表分为已反转的前缀 sll w_v l1sll w_v l1 和尚未处理的后缀 sll v_v l2sll v_v l2，二者与原始列表的关系由一条纯模型事实记录。循环入口处，该分支包含以下资源和事实（省略局部变量单元，保留引擎输出的顺序）：

fact (~(v_v == 0i)) **
fact (l == REVERSE l1 ++ l2) **
... **
sll v_v l2 **
sll w_v l1

fact (~(v_v == 0i)) **
fact (l == REVERSE l1 ++ l2) **
... **
sll v_v l2 **
sll w_v l1

声明式版本（10_reverse_decl.c10_reverse_decl.c）先完整写出希望写入状态的视图，再在目标树上后向证明这条蕴含：

PROOF {
  term target_symst = `exists l1 hd tl w_v v_v q.
    fact(l == (REVERSE l1) ++ (hd :: tl)) **
    fact(~(v_v == 0i)) **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr q **
    sll q tl **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre
  `;
  gnode root =
      gnode_new_with_ccl(mk_sl_ent(get_symbolic_state(), target_symst));
  /* 对 l2 分类讨论：空表分支与 ~(v_v == 0i) 矛盾；cons 分支展开 sll、
     提供存在量词例证，再框架消除其余资源。 */
  set_symbolic_state(gnode_prove(root));
}

PROOF {
  term target_symst = `exists l1 hd tl w_v v_v q.
    fact(l == (REVERSE l1) ++ (hd :: tl)) **
    fact(~(v_v == 0i)) **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr q **
    sll q tl **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre
  `;
  gnode root =
      gnode_new_with_ccl(mk_sl_ent(get_symbolic_state(), target_symst));
  /* 对 l2 分类讨论：空表分支与 ~(v_v == 0i) 矛盾；cons 分支展开 sll、
     提供存在量词例证，再框架消除其余资源。 */
  set_symbolic_state(gnode_prove(root));
}

目标已经确定了所需的结果：l2l2 必须分解为 hd :: tlhd :: tl，当前节点必须表示为两个字段资源，qq 指向保存 tltl 的链表。已反转的前缀和每一个局部变量单元也都必须一并写入目标，否则这条蕴含不成立。由于完整后件已经给定，自然可以采用目标导向的证明：分离逻辑的后向证明中的策略（CASES_TACCASES_TAC、变换、存在量词策略、AUTO_FRAME_SLTACAUTO_FRAME_SLTAC）逐步分解 current |-- targetcurrent |-- target，再由目标树验证组合出最终定理，交给 set_symbolic_stateset_symbolic_state。

操作式版本（10_reverse_op.c10_reverse_op.c）完全不声明目标。它指定一个操作，并提供参数来确定操作作用于哪里：

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 处的非空链表，并用这三个名字命名新产生的逻辑变量。”操作从当前资源中选出 sll v_v l2sll v_v l2（而不是 sll w_v l1sll w_v l1），对照分支中的事实检查非空前提，再实例化一条在声明时已经证明的引理，并把其余资源作为框架保留。最终提交的定理，与声明式版本手工证明的定理具有相同的形式。下一节将介绍如何声明 unfold_sll_not_nullunfold_sll_not_null，以及应用它时具体发生了什么。

操作的引理只涉及一小块足迹。以上面的展开为例，其背后的局部蕴含是：

~(v_v == 0i) ==>
  (sll v_v l2
   |--
   exists hd tl nxt.
     fact(l2 == hd :: tl) **
     data_at (field_addr v_v Tlist Fhead) Tint hd **
     data_at (field_addr v_v Tlist Ftail) Tptr nxt **
     sll nxt tl)

~(v_v == 0i) ==>
  (sll v_v l2
   |--
   exists hd tl nxt.
     fact(l2 == hd :: tl) **
     data_at (field_addr v_v Tlist Fhead) Tint hd **
     data_at (field_addr v_v Tlist Ftail) Tptr nxt **
     sll nxt tl)

而当前分支还持有已反转的前缀、模型事实和局部变量单元。操作式证明库的关键作用，就是把小足迹蕴含提升为完整状态的蕴含。

H ** F |-- H' ** F

H ** F |-- H' ** F

exists X. (H ** F) |-- exists X. (H' ** F)

exists X. (H ** F) |-- exists X. (H' ** F)

这正是前向证明一节介绍过的 local_apply(symhp, local_ent)local_apply(symhp, local_ent) 所做的事：它在分支的顶层分离合取项中定位局部前件，对照该分支的事实检查局部定理的纯前提（这里是 fact(~(v_v == 0i))fact(~(v_v == 0i))），将其余所有资源作为 保留，最后返回分支层面的蕴含定理。

完整的符号状态可能是若干分支的析取。得到每个分支的定理后，就可以利用析取单调性将它们组合起来：

|- symhp_1 || ... || symhp_n  |--  symhp_1' || ... || symhp_n'

|- symhp_1 || ... || symhp_n  |--  symhp_1' || ... || symhp_n'

整条证明生成链是：

local_ent
  -- local_apply：框架提升 + 存在量词提升 -->  分支蕴含
  -- 析取单调性 --------------------------->  完整状态蕴含
  -- set_symbolic_state ------------------->  提交后的新视图

local_ent
  -- local_apply：框架提升 + 存在量词提升 -->  分支蕴含
  -- 析取单调性 --------------------------->  完整状态蕴含
  -- set_symbolic_state ------------------->  提交后的新视图

操作式证明库把证明函数分为两个互补的层次。

这些函数不依赖具体数据结构，每个函数表达一种常见的状态调整意图：

当某个表示谓词反复用到同一种稳定的消耗/产出关系时，就可以把这种关系声明为一个领域操作，例如空链表与非空链表的展开与折叠、数组单元的聚焦、数组片段的切分与合并、未初始化区域的填充，以及树节点的展开与重新封装。调用时只需提供参数，说明操作“作用在哪里”；操作负责选择资源、检查纯前提、实例化已证明的引理并产出目标视图。

• 同一具体内存可以有多个分离逻辑视图；data_atdata_at 显式呈现可访问的单元，表示谓词则组织具体资源、功能模型及各视图之间的联系。
• 视图转换以 S |-- S'S |-- S' 定理为证明依据，不执行程序；local_applylocal_apply 通过框架提升与存在量词提升把小足迹蕴含应用于分支，并对照分支事实检查纯前提，再利用析取单调性合并各分支。
• 声明式推理写出完整目标；操作式推理指定操作，由证明库计算目标视图并生成蕴含定理。
• 证明库为常见的状态调整意图提供通用状态变换函数，为稳定的谓词转换提供领域操作。用户只需表达局部的推理意图，框架会自动保留，每一步提交的变化都有经内核检查的定理作为依据。