用策略纯化蕴含

EN | 中文

操作式证明部分以逐一命名每个资源步骤的方式验证了链表原地反转；本节回到声明式路线——写出循环不变式，让符号执行产生验证条件——并将这些条件的证明自动化。贯穿本节的示例是 cstar_examplescstar_examples 仓库中的 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（从 ww 出发）与未处理后缀 l2l2（从 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 |-- fact(l = REVERSE [] ++ l)
```
纯推理：不再讨论任何内存；剩下的是一条普通的列表等式：
```
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(y == x);


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(y == x);

程序变量的栈单元没有任何链表结构，因此通用库足以完全处理它们。但纯化并未完成：将 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 |-- fact(l = REVERSE [] ++ l)

其中不再有任何空间推理——但从语法上看，它仍然是分离逻辑蕴含，左侧是 empemp，右侧是一个 factfact。

从纯化目标到普通逻辑


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 定义了这一语言，并给出了为每条策略生成健全性条件的算法，将“这条策略是否健全”归约为“对应条件是否可证”。在其评估中，五个策略库共计 98 条策略，纯化了来自链式数据结构和微内核内存模块的 229 条蕴含中的 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 中对该引理的证明。

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

至此，PURIFY_TACPURIFY_TAC 只在显式构造的 VC 上运行过——而 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 = 0)) ** fact(l = x :: xs) **
  data_at (field_addr v Tlist Fhead) Tint x **
  sll q xs ** ...


exists x xs q.
  fact(~(v = 0)) ** fact(l = 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 是 int_array p x y lint_array p x y l 在索引 ii 处的单元被暂时取出后剩余的部分，即一个带空穴（hole）的数组。它保存了将单元放回并恢复完整数组的能力：


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` 编写策略