用策略纯化蕴含

EN | 中文

操作式证明部分逐一指定了操作资源的步骤，验证了链表的原地反转。本节回到声明式证明：写出循环不变式，让符号执行产生验证条件，再自动证明这些条件。贯穿本节的示例是 strategy_demo/examples/reverse_clean.cstrategy_demo/examples/reverse_clean.c，以及 strategy_demo/sll/strategy_demo/sll/ 和 strategy_demo/array/strategy_demo/array/ 中的策略文件。

两种推理

回顾反转的循环不变式：原列表 ll 分为已反转的前缀 l1l1 和尚未处理的后缀 l2l2，对应的链表分别以 ww 和 vv 为起点。在循环头部，引擎会产生一条建立 VC，要求进入循环时的状态蕴含不变式：

reversereverse 循环头部的建立 VC


data_at t__addr Tptr 0i **
data_at v__addr Tptr p__pre **
data_at w__addr Tptr 0i **
data_at p__addr Tptr p__pre **
sll p__pre l
|--
exists t_v v_v w_v l1 l2.
  fact (l == REVERSE l1 ++ l2) **
  data_at p__addr Tptr p__pre **
  data_at w__addr Tptr w_v **
  data_at v__addr Tptr v_v **
  data_at t__addr Tptr t_v **
  sll w_v l1 ** sll v_v l2


data_at t__addr Tptr 0i **
data_at v__addr Tptr p__pre **
data_at w__addr Tptr 0i **
data_at p__addr Tptr p__pre **
sll p__pre l
|--
exists t_v v_v w_v l1 l2.
  fact (l == REVERSE l1 ++ l2) **
  data_at p__addr Tptr p__pre **
  data_at w__addr Tptr w_v **
  data_at v__addr Tptr v_v **
  data_at t__addr Tptr t_v **
  sll w_v l1 ** sll v_v l2

要证明它，选取例证 t_v = 0t_v = 0、w_v = 0w_v = 0、v_v = p__prev_v = p__pre、l1 = []l1 = []、l2 = ll2 = l。接下来需要两种推理。

空间推理：将四对 data_atdata_at 一一匹配并消去；将 sll p__pre lsll p__pre l 与 sll p__pre l2sll p__pre l2 匹配；再根据 sll 0i l1sll 0i l1 所描述的链表位于空指针处，推出 l1 = []l1 = []。至此，VC 化简为：
```
emp |-- fact (l == REVERSE [] ++ l) ** emp
```
```
emp |-- fact (l == REVERSE [] ++ l) ** emp
```
纯推理：此时已不涉及内存，只剩下一条普通的列表等式：
```
l == REVERSE [] ++ l
```
```
l == REVERSE [] ++ l
```

两种推理需要不同的自动化方式。本节通过用户注册的策略（strategy）完成纯化（purification），自动处理空间推理；下一节再用 SMT 求解器完成纯推理。

起点：手工展开

reverse_clean.creverse_clean.c 给出了初次编写时的完整函数，其中包含契约、不变式，以及一条很长的 [[cst::assert(...)]][[cst::assert(...)]] 标注。这条标注手工将 sll v_v l2sll v_v l2 展开为头节点的两个字段单元，使 v->tailv->tail 的内存读取能够执行：


struct list *reverse(struct list *p)
  [[cst::param(`l:(int)list`)]]
  [[cst::require(`sll p l`)]]
  [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = (void *)0;
  struct list *v = p;
  struct list *t = (void *)0;
  PROOF term loop_inv = `exists l1 l2 w_v v_v t_v.
    fact(l = (REVERSE l1) ++ l2) **
    data_at p__addr Tptr p__pre **
    data_at w__addr Tptr w_v **
    data_at v__addr Tptr v_v **
    data_at t__addr Tptr t_v **
    sll w_v l1 **
    sll v_v l2
  `;
  while (v)
    [[cst::invariant(loop_inv)]]
  {
    [[cst::assert(`
      exists l1 l2 w_v v_v t_v x xs v_tail.
        fact(~(v_v == 0i)) **
        fact(l = (REVERSE l1) ++ l2) **
        fact(l2 == CONS x xs) **
        data_at p__addr Tptr p__pre **
        data_at w__addr Tptr w_v **
        data_at v__addr Tptr v_v **
        data_at t__addr Tptr t_v **
        sll w_v l1 **
        data_at (field_addr v_v Tlist Fhead) Tint x **
        data_at (field_addr v_v Tlist Ftail) Tptr v_tail **
        sll v_tail xs
    `)]]
    t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}


struct list *reverse(struct list *p)
  [[cst::param(`l:(int)list`)]]
  [[cst::require(`sll p l`)]]
  [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = (void *)0;
  struct list *v = p;
  struct list *t = (void *)0;
  PROOF term loop_inv = `exists l1 l2 w_v v_v t_v.
    fact(l = (REVERSE l1) ++ l2) **
    data_at p__addr Tptr p__pre **
    data_at w__addr Tptr w_v **
    data_at v__addr Tptr v_v **
    data_at t__addr Tptr t_v **
    sll w_v l1 **
    sll v_v l2
  `;
  while (v)
    [[cst::invariant(loop_inv)]]
  {
    [[cst::assert(`
      exists l1 l2 w_v v_v t_v x xs v_tail.
        fact(~(v_v == 0i)) **
        fact(l = (REVERSE l1) ++ l2) **
        fact(l2 == CONS x xs) **
        data_at p__addr Tptr p__pre **
        data_at w__addr Tptr w_v **
        data_at v__addr Tptr v_v **
        data_at t__addr Tptr t_v **
        sll w_v l1 **
        data_at (field_addr v_v Tlist Fhead) Tint x **
        data_at (field_addr v_v Tlist Ftail) Tptr v_tail **
        sll v_tail xs
    `)]]
    t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}

这个文件在提交时还无法通过验证：上面的建立 VC、循环体末尾的保持 VC、循环之后的后置条件 VC，以及断言自身的 VC 都保持开放。无论采用后向策略还是操作式步骤，逐一手工卸除这些 VC 都需要重复相同的匹配与展开操作。本节接下来介绍如何自动完成这些工作，并省去那条很长的断言。

`PURIFY_TACPURIFY_TAC`


PROOF gnode PURIFY_TAC(gnode gn);


PROOF gnode PURIFY_TAC(gnode gn);

PURIFY_TACPURIFY_TAC 接收一个结论为分离逻辑蕴含的目标，反复对它应用当前已注册的策略，再返回纯化后仍需证明的目标。没有策略可以匹配时，它就会停止；单次调用不必解决整个目标。这一过程不回溯：一旦某条策略触发，这一步就不可撤销，即使后续证明受阻也一样。因此，改写过于激进的策略可能将可证目标变为不可证目标，不应注册这样的策略。

要观察它在建立 VC 上的效果，在不变式与 whilewhile 之间插入一个证明块：


PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
}


PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
}

PURIFY_TACPURIFY_TAC 返回的目标


sll p__pre l
|--
exists l1 l2.
  fact (l == REVERSE l1 ++ l2) **
  sll 0i l1 **
  sll p__pre l2


sll p__pre l
|--
exists l1 l2.
  fact (l == REVERSE l1 ++ l2) **
  sll 0i l1 **
  sll p__pre l2

四对 data_atdata_at 已全部消去，存在变量 t_vt_v、w_vw_v、v_vv_v 也已实例化，而我们还没有编写任何规则。这是因为 C* 默认注册了通用库 $CSTAR_HOME/include/common.strategies$CSTAR_HOME/include/common.strategies，其中的规则可以处理存在变量实例化和 data_atdata_at。其中的 data_atdata_at 规则依据一个简单的事实：同一地址、同一类型的两个 data_atdata_at 必须存储相同的值，然后就可以消去两侧的资源。将这一过程归结为一条规则，效果如下（库中实际使用了分阶段执行的多条规则）：


left  : data_at(?p, ?ty, ?x) at 0
right : data_at(p, ty, ?y) at 1
action :
  left_erase(0);
  right_erase(1);
  right_add(x == y);


left  : data_at(?p, ?ty, ?x) at 0
right : data_at(p, ty, ?y) at 1
action :
  left_erase(0);
  right_erase(1);
  right_add(x == y);

程序变量的栈单元没有任何链表结构，因此通用库足以完全处理它们。但纯化到这里就无法继续了：要将 sll p__pre lsll p__pre l 与 sll p__pre l2sll p__pre l2 匹配，或从 sll 0i l1sll 0i l1 推出 l1 = []l1 = []，都需要关于 sllsll 的知识，通用库无法提供这些知识。

为 `sllsll` 编写策略

strategy_demo/sll/sll.strategiesstrategy_demo/sll/sll.strategies 用五条声明式规则提供了这些知识。完成建立 VC 的纯化需要其中两条。第一条是“空指针即空列表”规则：


id : 0
priority : core(0)
right : sll(0, ?l) at 0
action : right_erase(0);
         right_add(l == NIL{Z});


id : 0
priority : core(0)
right : sll(0, ?l) at 0
action : right_erase(0);
         right_add(l == NIL{Z});

第二条是“同地址链表消去”规则：


id : 1
priority : core(0)
left : sll(?p, ?l1) at 0
right : sll(p, ?l2) at 1
action : left_erase(0);
         right_erase(1);
         right_add(l2 == l1);


id : 1
priority : core(0)
left : sll(?p, ?l1) at 0
right : sll(p, ?l2) at 1
action : left_erase(0);
         right_erase(1);
         right_add(l2 == l1);

一条规则由六个字段构成：

字段	含义
`idid`	规则在其策略文件中的编号
`prioritypriority`	调度的优先级与匹配阶段；本例保持默认配置
`leftleft`	在蕴含左侧（前件）匹配的断言
`rightright`	在右侧（后件）匹配的断言
`checkcheck`	在动作执行前必须满足的条件
`actionaction`	状态变更：删除或添加断言，实例化存在变量

?p?p 和 ?l1?l1 是模式变量；后续不带问号的 pp、l1l1 指本次匹配所绑定的值。 at 0at 0、at 1at 1 是位置标签，动作通过它们引用匹配到的断言。 leftleft 与 rightright 仅指 H |-- KH |-- K 的左右两侧，没有其他含义。

注册策略文件时需要提供路径和文件名；reverse.creverse.c 根据自身的 __FILE____FILE__ 定位文件夹：


PROOF static int install_sll_strategy(void) {
  char *source_path = strdup(__FILE__);
  char *strategy_folder = gc_sprintf(
    "%s/sll", dirname(dirname(source_path)));
  cst_add_strategy_folder_path(strategy_folder);
  cst_add_strategy_to_header("sll.strategies");
  return 0;
}
PROOF static int _install_sll_strategy = install_sll_strategy();


PROOF static int install_sll_strategy(void) {
  char *source_path = strdup(__FILE__);
  char *strategy_folder = gc_sprintf(
    "%s/sll", dirname(dirname(source_path)));
  cst_add_strategy_folder_path(strategy_folder);
  cst_add_strategy_to_header("sll.strategies");
  return 0;
}
PROOF static int _install_sll_strategy = install_sll_strategy();

注册后，在建立 VC 上再次运行 PURIFY_TACPURIFY_TAC。通用库处理 data_atdata_at，这两条规则处理 sllsll，目标变为：


emp |-- fact (l == REVERSE [] ++ l) ** emp


emp |-- fact (l == REVERSE [] ++ l) ** emp

这个目标已不需要空间推理，但在语法上仍是分离逻辑蕴含：左侧是 empemp，右侧是一个 factfact，后面还有一个 empemp。

从纯化目标到普通逻辑


PROOF gnode POST_PURIFY_TAC(gnode gn);


PROOF gnode POST_PURIFY_TAC(gnode gn);

POST_PURIFY_TACPOST_PURIFY_TAC 接收一个不再持有实际空间资源的分离逻辑目标，合并剩余的 factfact，移动其中的存在量词，再将得到的 factfact/empemp 蕴含改写为普通逻辑目标。这一步不应用任何策略，只负责最后的转换，将纯化结果变为纯推理目标。

补全证明块：


PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  /* g 的结论现在是一条普通逻辑公式 */
}


PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  /* g 的结论现在是一条普通逻辑公式 */
}

目标变为：


l == REVERSE [] ++ l


l == REVERSE [] ++ l

我们暂时不证明这个目标。现在，需要解决的问题已从内存资源之间的对应关系变成了一条普通的列表等式。纯化到此结束，接下来由 SMT 求解器继续处理。

策略为何健全

策略对公式的改写也需要依据。从概念上说，每条策略都对应一条带有适用条件的分离逻辑引理。例如，“同地址链表消去”需要下面这条蕴含作为依据。消去 sll p l1sll p l1 与 sll p l2sll p l2 后，仍须证明纯事实 l2 = l1l2 = l1：


sll p l1 |-- forall l2. fact(l2 = l1) -* sll p l2


sll p l1 |-- forall l2. fact(l2 = l1) -* sll p l2

对于带有 checkcheck 的规则，检查条件会成为相应健全性义务的前提。

这里使用的策略语言是 Stellis；论文 Stellis: A Strategy Language for Purifying Separation Logic Entailments 定义了这一语言，并给出了为每条策略生成健全性条件的算法，将“这条策略是否健全”归约为“对应条件是否可证”。论文评估了来自链式数据结构和微内核内存模块的 229 条蕴含；五个策略库中的 98 条策略成功纯化了其中 219 条。

本示例中的健全性引理已手工写出并证明：

strategy_demo/sll/strategy_proof.hstrategy_demo/sll/strategy_proof.h 和 strategy_proof.cstrategy_proof.c：sll.strategiessll.strategies 每条规则对应一条引理（文件中的引理编号不遵循规则 id）；
strategy_demo/array/strategy_proof.hstrategy_demo/array/strategy_proof.h 和 strategy_proof.cstrategy_proof.c：类似地，对应下文的 array.strategiesarray.strategies。

因此，要理解一条策略，需要对照阅读三项内容：.strategies.strategies 文件中的匹配与动作、strategy_proof.hstrategy_proof.h 中陈述的健全性引理，以及 strategy_proof.cstrategy_proof.c 中对该引理的证明。

当前的信任边界

C* 尚未接入完整的检查流程：自动生成每条已注册策略的健全性引理，并在加载时检查其证明。演示目录提供了健全性证明，但运行时并未将已注册策略与这些证明绑定；PURIFY_TACPURIFY_TAC / POST_PURIFY_TACPOST_PURIFY_TAC 适配器通过显式的信任假设来确认结果，并未通过推导规则重建证明。现阶段，已注册策略与纯化桥接都属于可信计算基：如果某条策略有误，系统尚无法排除由此产生的不健全结论。验证报告会明确记录这两类依赖。桥接的 factfact 引理会列在报告的 axiomsaxioms 数组中。纯化后的目标解决后，PURIFY_TACPURIFY_TAC 还需凭借一条蕴涵式，将这一结果作为原蕴含的证明接受；这条蕴涵式也会列在该数组中。每个已注册的策略文件则列在 strategiesstrategies 中。因此，从报告中可以区分一次运行是否依赖这些假设和策略。与此相关，工具链随附的 AI 助手指南指出，这些策略钩子并不稳定，建议助手改用按名称显式引用引理的证明步骤。本部分教程介绍策略，是为了演示课程中的这一方法。

框架推断：同样的纯化，另一个入口

到目前为止，我们只在显式构造的 VC 上运行过 PURIFY_TACPURIFY_TAC。reverse_clean.creverse_clean.c 中仍保留着那条很长的 [[cst::assert]][[cst::assert]]，它仅用于显式展开头节点，以便读取 v->tailv->tail。 sll.strategiessll.strategies 余下的三条规则使该断言不再必要：注册完整文件后，直接删除断言即可，t = v->tail;t = v->tail; 也不再因 Cannot derive the precondition of Memory ReadCannot derive the precondition of Memory Read 而失败。下面来看这为什么可行。

一次内存读取究竟需要什么

当符号执行引擎执行 v->tailv->tail 时，必须从当前状态中切出该字段的读取权限。抽象地说，引擎需要找到一个未知的剩余部分 ?H?H，使以下蕴含成立：


fact(~(v = 0)) ** sll v l ** ...
|--
exists val.
  data_at (field_addr v Tlist Ftail) Tptr val ** ?H


fact(~(v = 0)) ** sll v l ** ...
|--
exists val.
  data_at (field_addr v Tlist Ftail) Tptr val ** ?H

右侧的 data_atdata_at 是这次读取所需的资源；?H?H 是读取之后仍应保留的其余状态。计算 ?H?H 的过程就是框架推断（frame inference）。这是符号执行在每次内存访问时的内部步骤，并非交给用户的额外 VC。

纯化为何能解决它

考虑 sll.strategiessll.strategies 的展开规则：


id : 4
priority : core(0)
left : sll(?p, ?l) at 0
       (p != 0) at 1
right : data_at(field_addr(p, list, tail), PTR(struct list), ?v) at 2
action : left_erase(0);
         left_exist_add(x);
         left_exist_add(xs);
         left_exist_add(q);
         left_add(data_at(field_addr(p, list, head), I32, x));
         left_add(data_at(field_addr(p, list, tail), PTR(struct list), q));
         left_add(sll(q, xs));
         left_add(l == CONS{Z}(x, xs));


id : 4
priority : core(0)
left : sll(?p, ?l) at 0
       (p != 0) at 1
right : data_at(field_addr(p, list, tail), PTR(struct list), ?v) at 2
action : left_erase(0);
         left_exist_add(x);
         left_exist_add(xs);
         left_exist_add(q);
         left_add(data_at(field_addr(p, list, head), I32, x));
         left_add(data_at(field_addr(p, list, tail), PTR(struct list), q));
         left_add(sll(q, xs));
         left_add(l == CONS{Z}(x, xs));

当左侧持有非空的 sll p lsll p l、右侧恰好需要该节点的 tailtail 单元时，这条规则触发，在左侧将链表展开一层。随后，通用的 data_atdata_at 策略将展开得到的 tailtail 单元与右侧所需的单元匹配，并消去两者。纯化停止时，左侧持有：


exists x xs q.
  fact (~(v == 0i)) ** fact (l2 == x :: xs) **
  data_at (field_addr v Tlist Fhead) Tint x **
  sll q xs ** ...


exists x xs q.
  fact (~(v == 0i)) ** fact (l2 == x :: xs) **
  data_at (field_addr v Tlist Fhead) Tint x **
  sll q xs ** ...

这次读取没有取走的资源，恰好就是应当填入 ?H?H 的剩余部分。换句话说，框架推断的目标本身就是一条分离逻辑蕴含。将所需资源匹配消去，并保留其余资源，正是纯化所做的工作，因此可以直接复用同一套策略。

从 QCP 到用户层

框架推断由底层 QCP 符号执行引擎执行，而策略原本就是驱动 QCP 自动化的组件。 C* 在用户层提供了设置策略路径和注册策略的接口：


cst_add_strategy_folder_path(strategy_folder);
cst_add_strategy_to_header("sll.strategies");


cst_add_strategy_folder_path(strategy_folder);
cst_add_strategy_to_header("sll.strategies");

因此，写在 C* 文件中的注册代码，也能定制引擎在内存访问时完成框架推断的方式。这也解释了为什么补全一个 .strategies.strategies 文件会同时带来两种效果：显式构造的 PURIFY_TACPURIFY_TAC 目标得以通过，原先需要那条很长的断言才能继续的读取也能自动执行。

sll.strategiessll.strategies 的五条规则分工如下：

id	触发位置	效果
`00`	右侧的 `sll 0 lsll 0 l`	将空指针链表替换为 `l = []l = []`
`11`	两侧同地址的 `sllsll`	消去空间谓词，留下列表等式
`22`	左侧头单元，右侧需要 `sllsll`	展开右侧目标，使链表可重新折叠
`33`	左侧 `sll p lsll p l` 且 `p = 0p = 0`	消去空链表，添加 `l = []l = []`
`44`	左侧非空 `sllsll`，右侧需要 `tailtail` 单元	展开一层节点，支持读取与框架推断

数组的策略

除了链表，数组也需要空间推理。数组策略引入了一个新要素：通过算术推理检查规则的适用条件。谓词和规则位于 strategy_demo/array/strategy_demo/array/ 中。

int_arrayint_array 谓词

int_array p x y lint_array p x y l 描述以 pp 为基地址、索引位于半开区间 [x, y)[x, y) 内的连续 intint 单元；逻辑列表 ll 按顺序记录其中存储的值。该谓词通过对列表递归来定义：


int_array p x y []
  -|- fact(x = y)
int_array p x y (h :: t)
  -|- data_at (p + x * sizeof Tint) Tint h **
      int_array p (x + 1i) y t


int_array p x y []
  -|- fact(x = y)
int_array p x y (h :: t)
  -|- data_at (p + x * sizeof Tint) Tint h **
      int_array p (x + 1i) y t

因此 data_at q Tint vdata_at q Tint v 表示对单个 intint 单元的所有权，而 int_array p x y lint_array p x y l 表示对 [x, y)[x, y) 中每一个单元的所有权；例如，int_array p 0i 3i [a; b; c]int_array p 0i 3i [a; b; c] 展开为分离合取：


data_at (p + 0i * sizeof Tint) Tint a **
data_at (p + 1i * sizeof Tint) Tint b **
data_at (p + 2i * sizeof Tint) Tint c


data_at (p + 0i * sizeof Tint) Tint a **
data_at (p + 1i * sizeof Tint) Tint b **
data_at (p + 2i * sizeof Tint) Tint c

当一次读写只需要单元 ii 的 data_atdata_at 时，我们需要从所拥有的数组区段中切出这个单元，同时保留其余部分，并非将整个数组变为一个 data_atdata_at。

int_array_with_holeint_array_with_hole 谓词

int_array_with_hole p x y i lint_array_with_hole p x y i l 描述这样一个带空洞（hole）的数组：从 int_array p x y lint_array p x y l 中暂时取出索引 ii 处的单元，保留其余部分。它保存了将单元放回并恢复完整数组的能力：


int_array_with_hole p x y i l
  -|-
  forall v.
    data_at (p + i * sizeof Tint) Tint v -*
    int_array p x y (replace_inth (i - x) v l)


int_array_with_hole p x y i l
  -|-
  forall v.
    data_at (p + i * sizeof Tint) Tint v -*
    int_array p x y (replace_inth (i - x) v l)

这里 -*-* 是分离蕴含（separating implication，即魔术棒）：将索引 ii 处值为 vv 的单元填回空洞，就能恢复 [x, y)[x, y) 上的完整数组。恢复后的逻辑列表，是在原列表 ll 的相对索引 i - xi - x 处写入 vv 的结果，即 replace_inth (i - x) v lreplace_inth (i - x) v l。

strategy_demo/array/array.strategiesstrategy_demo/array/array.strategies 包含三条规则：

id	匹配侧	改写效果
`00`	左: `int_array p x y lint_array p x y l`；右: 索引 `ii` 的 `data_atdata_at`	检查 `x <= i < yx <= i < y`；左侧数组变为空洞形式，右侧单元变为 `v = inth (i-x) lv = inth (i-x) l`
`11`	左: `int_array_with_hole p x y i l1int_array_with_hole p x y i l1`；右: `int_array p x y l2int_array p x y l2`	消去两者；在右侧引入值 `vv`、索引 `ii` 处的 `data_atdata_at`，以及 `l2 = replace_inth (i-x) v l1l2 = replace_inth (i-x) v l1`
`22`	左: `int_array p x y l1int_array p x y l1`；右: `int_array p x y l2int_array p x y l2`	消去两个数组谓词，留下 `l2 = l1l2 = l1`

下面完整列出规则 00：


id : 0
priority : core(0)
left : int_array(?p, ?x, ?y, ?l) at 0
right : data_at(p + ?i * sizeof(I32), I32, ?v) at 1
check : infer(x <= i);
        infer(i < y);
action : left_erase(0);
         right_erase(1);
         left_add(int_array_with_hole(p, x, y, i, l));
         right_add(v == inth(i - x, l));


id : 0
priority : core(0)
left : int_array(?p, ?x, ?y, ?l) at 0
right : data_at(p + ?i * sizeof(I32), I32, ?v) at 1
check : infer(x <= i);
        infer(i < y);
action : left_erase(0);
         right_erase(1);
         left_add(int_array_with_hole(p, x, y, i, l));
         right_add(v == inth(i - x, l));

当右侧需要数组 pp 在索引 ii 处的单元时，仅匹配地址的形式，还不足以切出该单元；规则还必须确认 ii 位于 [x, y)[x, y) 内。这就是 checkcheck 字段中两行 inferinfer 的作用：它们要求 QCP 的内置求解器从当前纯事实中推出 x <= ix <= i 与 i < yi < y，只有两次推理都成功，动作才会执行。（该内置求解器只决定局部的规则适用性；它并非下一节的 SMT 集成，后者用于解决整个纯目标。）

数组策略的注册过程封装在 strategy_demo/array/array.cstrategy_demo/array/array.c 的安装函数中，该函数可以复用，且具有幂等性：


PROOF int install_strategy_demo_array(void) {
  static bool installed = false;
  if (installed) return 0;
  cst_add_strategy_folder_path(dirname(strdup(__FILE__)));
  cst_add_strategy_to_header("array.strategies");
  smt_init();
  smt_register_seq_handler();
  installed = true;
  return 0;
}


PROOF int install_strategy_demo_array(void) {
  static bool installed = false;
  if (installed) return 0;
  cst_add_strategy_folder_path(dirname(strdup(__FILE__)));
  cst_add_strategy_to_header("array.strategies");
  smt_init();
  smt_register_seq_handler();
  installed = true;
  return 0;
}

两个 smt_smt_ 调用还初始化了 SMT 相关功能。下一节将介绍这两个调用，并完成数组示例。

小结

一条验证条件同时涉及空间推理（资源之间的对应关系）与纯推理（列表等式、整数边界）；纯化自动完成空间推理，将剩余的纯推理转换为普通逻辑目标。
PURIFY_TACPURIFY_TAC 应用已注册的策略，直到没有策略可以匹配为止，且不回溯；默认的 common.strategiescommon.strategies 处理存在变量实例化与 data_atdata_at，sll.strategiessll.strategies 这样的用户文件则为各个谓词补充展开、折叠与消去规则。
POST_PURIFY_TACPOST_PURIFY_TAC 将纯化后的 factfact/empemp 蕴含转换为普通逻辑公式，这是纯化的终点。
每条策略对应一条分离逻辑引理；Stellis 语言使这一对应系统化，但在当前实现中，已注册策略与纯化桥接仍位于可信计算基之中。
内存访问时的框架推断本身就是一条蕴含，因此也能使用同一套策略：注册一个 .strategies.strategies 文件既能卸除显式 VC，也能自动执行读写，访问数据结构谓词所描述的资源。sllsll 可以这样处理，数组区段也可以，只是数组规则还需要 checkcheck 检查。

用策略纯化蕴含

两种推理

起点：手工展开

PURIFY_TACPURIFY_TAC

为 sllsll 编写策略

从纯化目标到普通逻辑

策略为何健全

框架推断：同样的纯化，另一个入口

一次内存读取究竟需要什么

纯化为何能解决它

从 QCP 到用户层

数组的策略

小结

`PURIFY_TACPURIFY_TAC`

为 `sllsll` 编写策略