有证明的视图转换

在前向证明一节中，链表反转的循环在读取 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(l == REVERSE l1 ++ l2) **
fact(~(v_v == 0i)) **
sll w_v l1 **
sll v_v l2 **
...

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

声明式版本（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 通过框架提升与存在量词提升把小足迹蕴含作用于分支，并把纯前提作为分支事实加以检查，析取单调性再合并各分支。
• 声明式推理写出完整目标；操作式推理指定操作，由证明库计算目标视图并生成蕴含定理。
• 证明库为常见塑形意图提供通用状态变换函数，为稳定的谓词转换提供领域操作——推理意图局部化，框架自动保留，而提交的每一步变化始终是经内核检查的定理。