C*：开发与证明一体化

证明-规约-实现（PSI）胶囊

EN | 中文

经过验证的库应当像普通库一样使用：客户端包含头文件，调用函数，就可以继续后面的工作。本节展示 C* 如何做到这一点。核心思想是将三种容易彼此脱节的产物放在一起：一段 C 实现、客户端使用这段实现时所依据的规约，以及证明实现符合规约的证明代码。它们共同组成一个带契约的函数，称为证明-规约-实现胶囊（PSI 胶囊，简称 Ψ-胶囊）。一旦胶囊通过验证，契约就保障了每次调用的安全性，胶囊内部的证明工作也不会在调用处重复。

重复证明的代价

再来看前向证明一节中的链表反转循环。循环体执行四条普通的 C 语句，其中两条需要访问的内存，在符号状态中仅由抽象谓词 sllsll 描述。在读取或写入 v->tailv->tail 之前，必须先暴露 vv 处的节点；写入之后，又必须恢复不变式：

// v != 0, so l2 is a cons: unfold sll vv l2 into its head/tail cells.
[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`l2:(int)list`, spec_rule(`vv:addr`, sll_unfold)));
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}
struct list *t = v->tail;
v->tail = w;
w = v;
v = t;
// Re-establish the invariant: fold the node back onto the reversed prefix.
[[cst::proof]] {
  // ... a REVERSE/APPEND equation rev_eq is proved here first ...
  thm fold = undisch_rule(spec_rule(`wv:addr`,
      spec_rule(`REVERSE (l1:(int)list)`,
          spec_rule(`xv:int`, spec_rule(`vv:addr`, sll_fold)))));
  thm ent = rewrite_rule(THM_LIST(gsym_rule(rev_eq)), fold);
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}
// v != 0, so l2 is a cons: unfold sll vv l2 into its head/tail cells.
[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`l2:(int)list`, spec_rule(`vv:addr`, sll_unfold)));
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}
struct list *t = v->tail;
v->tail = w;
w = v;
v = t;
// Re-establish the invariant: fold the node back onto the reversed prefix.
[[cst::proof]] {
  // ... a REVERSE/APPEND equation rev_eq is proved here first ...
  thm fold = undisch_rule(spec_rule(`wv:addr`,
      spec_rule(`REVERSE (l1:(int)list)`,
          spec_rule(`xv:int`, spec_rule(`vv:addr`, sll_fold)))));
  thm ent = rewrite_rule(THM_LIST(gsym_rule(rev_eq)), fold);
  cst_set_symbolic_state(
      local_apply(cst_get_symbolic_state(), ent));
}

我们有必要为这一模式取一个名字，因为在每个访问抽象数据结构的程序点，它都会再次出现：

展开当前视图（sll、数组谓词等）
  -> 暴露底层的 data_at 单元
  -> 执行那一次内存读取或写入
  -> 恢复本次写入所破坏的任何不变式
  -> 将高层视图折叠回去
展开当前视图（sll、数组谓词等）
  -> 暴露底层的 data_at 单元
  -> 执行那一次内存读取或写入
  -> 恢复本次写入所破坏的任何不变式
  -> 将高层视图折叠回去

把这些步骤直接写在访问处，会带来两方面的代价。

证明重复。展开-重新折叠步骤仅依赖谓词的形状，与所在的函数无关。如果十个函数各写入一次 tailtail 字段，就需要十份本质上相同的证明代码；一旦谓词的定义发生变化，这十份代码都需要维护。

抽象泄漏。客户端的证明必须涉及 field_addrfield_addr、data_atdata_at 和谓词的内部存在量词。引入谓词，是为了让客户端能用“一个内容为 ll 的链表”来推理；把展开-折叠步骤直接写在客户端中，又会迫使每个客户端处理底层表示。

操作式机制已经能够封装可复用的步骤：上面的展开步骤只需声明为一个操作，就可以在任何地方使用。 PSI 胶囊则将代码连同其步骤一并封装，使调用处完全不含证明代码。

胶囊的结构

具体来说，胶囊是一个带契约的普通 C 函数，函数体构成一个证明三明治：先用证明代码打开抽象层，再执行一条（或几条）裸 C 语句，最后用证明代码将其折叠回去。契约只需写成一个宏，供头文件中的声明和源文件中的定义共同使用：

unit.h :  #define FOO_SPEC                       // 唯一的契约宏
            [[cst::param(...)]]                  //   = 安全接口
            [[cst::require(...)]]
            [[cst::ensure(...)]]
          ret foo(args) FOO_SPEC;                // 声明复用该宏
          // 以及对契约所用定义模块的 #require
unit.c :  ret foo(args) FOO_SPEC {               // 定义复用相同的宏
            [[cst::proof]] { open_X(...); }      // 证明：暴露底层单元
            /* 一次真正的 C 读取或写入 */         // 实现
            [[cst::proof]] { close_X(...); }     // 证明：恢复不变式，重新折叠
          }
client :  #include "unit.h"
          #require "unit.c"
          ... foo(args) ...                      // 普通的 C 调用，不含证明代码
unit.h :  #define FOO_SPEC                       // 唯一的契约宏
            [[cst::param(...)]]                  //   = 安全接口
            [[cst::require(...)]]
            [[cst::ensure(...)]]
          ret foo(args) FOO_SPEC;                // 声明复用该宏
          // 以及对契约所用定义模块的 #require
unit.c :  ret foo(args) FOO_SPEC {               // 定义复用相同的宏
            [[cst::proof]] { open_X(...); }      // 证明：暴露底层单元
            /* 一次真正的 C 读取或写入 */         // 实现
            [[cst::proof]] { close_X(...); }     // 证明：恢复不变式，重新折叠
          }
client :  #include "unit.h"
          #require "unit.c"
          ... foo(args) ...                      // 普通的 C 调用，不含证明代码
产物 所在位置 使用者
规约 共享的 *_SPEC*_SPEC 契约宏 客户端，每次调用处
实现 函数体中的裸 C 语句 编译后的程序
证明 包裹其外的 [[cst::proof]][[cst::proof]] 块 验证器，一次

实际开发中还有两条重要约定。

客户端通过 #include#include + #require#require 接入胶囊。头文件提供契约和谓词声明；#require#require 告知验证器（已通过验证的）定义所在的位置。头文件自身也可以用 #require#require 引入契约所依赖的模块；这些依赖具有传递性，工具也会对它们去重，因此客户端只需指定要使用的单元。之后，调用胶囊就是依据其契约进行符号执行，与调用任何契约函数完全相同。

胶囊位于谓词层次中的特定层次上。像 sllsll 这样的谓词位于 data_atdata_at 之上；开发更复杂的程序时，还可以在其上增加更多层次。每个胶囊的契约都有固定的层次。调用方可以选择与当前符号状态匹配的胶囊，不必为了使用较低层次的接口而手动展开谓词。同一条底层语句，比如一次字段写入，可以通过不同层次上的胶囊提供不同的接口。

首批胶囊：数组单元访问

第一组胶囊从最小的实现开始：在字节缓冲区的抽象视图下，封装一次数组下标访问。该谓词是对标准库 array_atarray_at 的单态封装：

PROOF thm char_array_def = new_fun_definition(
    `char_array (p:addr) (xs:(int)list) : hprop =
       array_at p Tchar (ilength xs) xs`);
PROOF thm char_array_def = new_fun_definition(
    `char_array (p:addr) (xs:(int)list) : hprop =
       array_at p Tchar (ilength xs) xs`);

char_array p xschar_array p xs 表示 pp 指向一个字节数组，其内容为逻辑列表 xsxs；数组的长度就是列表自身的长度。标准库使用整数索引运算符处理列表：ilength xsilength xs 表示长度，inth i xsinth i xs 表示索引 ii 处的元素，replace_inth i v xsreplace_inth i v xs 表示将该元素替换为 vv 后的列表。下文的契约沿用这套记号。

该单元发布两个胶囊。它们的契约即安全接口：

#define CHAR_ARRAY_READ_SPEC                                                  \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf xs ** fact(__return == inth i xs)`)]]
#define CHAR_ARRAY_WRITE_SPEC                                                 \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf (replace_inth i ch xs)`)]]
char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC;
void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC;
#define CHAR_ARRAY_READ_SPEC                                                  \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf xs ** fact(__return == inth i xs)`)]]
#define CHAR_ARRAY_WRITE_SPEC                                                 \
  [[cst::param(`xs:(int)list`)]]                                              \
  [[cst::require(`char_array buf xs ** fact(n == ilength xs) ** fact(0i <= i) ** fact(i < n)`)]] \
  [[cst::ensure(`char_array buf (replace_inth i ch xs)`)]]
char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC;
void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC;

（宏形式有一项特殊限制：反引号引用必须完整地写在宏的同一行内，因此 require 子句即使很长，也无法换行。）

require 子句的含义是：调用方拥有该数组，保证 nn 等于数组长度，且 ii 在边界之内。注意，界内访问需要的恰好就是这三条事实：它们既构成安全接口，也是内部安全论证的依据，只需陈述一次。

写胶囊。其定义展开相同的 CHAR_ARRAY_WRITE_SPECCHAR_ARRAY_WRITE_SPEC 宏，包裹一条裸存储语句：

void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  buf[i] = ch;
  [[cst::proof]] { close_char_array_write(`buf__pre:addr`, `i__pre:int`); }
}
void char_array_write(char *buf, int n, int i, char ch) CHAR_ARRAY_WRITE_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  buf[i] = ch;
  [[cst::proof]] { close_char_array_write(`buf__pre:addr`, `i__pre:int`); }
}

open_char_arrayopen_char_array 是一个封装好的操作，在单元中只需声明一次，并以一条已证明的引理为依据。来看它的声明模式，理解前几节介绍的操作式风格如何用于这个例子：

decl_operation(open_char_array_op,
  TERM_LIST(`p:addr`, `i:int`),
  TERM_LIST(`char_array (KEY (p:addr)) (CAPTURE (xs:(int)list))`),
  TERM_LIST(`0i <= (i:int)`, `i < ilength (xs:(int)list)`),
  `data_at (p + i * sizeof Tchar) Tchar (inth i xs) **
   char_array_hole p i xs`)
decl_operation(open_char_array_op,
  TERM_LIST(`p:addr`, `i:int`),
  TERM_LIST(`char_array (KEY (p:addr)) (CAPTURE (xs:(int)list))`),
  TERM_LIST(`0i <= (i:int)`, `i < ilength (xs:(int)list)`),
  `data_at (p + i * sizeof Tchar) Tchar (inth i xs) **
   char_array_hole p i xs`)

它消耗 pp 处的 char_arraychar_array 资源（捕获当前列表 xsxs），检查两条边界事实，并产出裸 data_atdata_at 形式的单元 ii，以及 char_array_hole p i xschar_array_hole p i xs。后者表示分离出单元 ii 后，数组的剩余部分。观察函数体中的符号状态变化可以看清整个过程。打开之后：

此时，裸语句 buf[i] = ch;buf[i] = ch; 只是向普通的 data_atdata_at 单元写入数据，符号执行引擎可以直接处理，无需任何证明代码：

只有当前访问的单元发生了变化：inth i__pre xsinth i__pre xs 变成了 ch__prech__pre。最后，close_char_array_writeclose_char_array_write 将空洞和更新后的单元折叠回完整的数组，使这次对单个单元的写入在抽象视图中表现为一次列表更新：

最终状态与后置条件匹配，胶囊通过验证，没有遗留的 VC。

读胶囊。有一个小细节：位于 returnreturn 之后的证明块已没有可供变换的符号状态，因此有返回值的胶囊会先将结果读入局部变量，在返回之前把数组折叠回去：

char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  char ch = buf[i];
  [[cst::proof]] { close_char_array_read(`buf__pre:addr`, `i__pre:int`); }
  return ch;
}
char char_array_read(char *buf, int n, int i) CHAR_ARRAY_READ_SPEC
{
  [[cst::proof]] { open_char_array(`buf__pre:addr`, `i__pre:int`); }
  char ch = buf[i];
  [[cst::proof]] { close_char_array_read(`buf__pre:addr`, `i__pre:int`); }
  return ch;
}

三明治结构保持完整；只是裸代码段从一条语句变成了两条。读操作和写操作在关闭步骤中依赖的纯引理有所不同：读取后，单元中仍然保存着 inth i xsinth i xs，因此折叠时需要用到 replace_inth i (inth i xs) xsreplace_inth i (inth i xs) xs 就是 xsxs 本身这一性质。该单元一次性证明了几条简单的列表引理，这就是其中之一；这些引理与使用它们的操作放在一起。

客户端。单元通过验证后，客户端包含头文件，用 #require#require 引入源文件，然后以普通 C 调用的形式使用胶囊：

#include "psi_examples/units/char_array_unit.h"
#require "psi_examples/units/char_array_unit.c"
char write_then_read(char *buf, int n, int i, char ch)
    [[cst::param(`xs:(int)list`)]]
    [[cst::require(`char_array buf xs ** fact(n == ilength xs)
                    ** fact(0i <= i) ** fact(i < n)`)]]
    [[cst::ensure(`char_array buf (replace_inth i ch xs)
                   ** fact(__return == ch)`)]]
{
  char_array_write(buf, n, i, ch);
  [[cst::proof]] { /* pure-fact glue: replace_inth preserves ilength */ }
  char got = char_array_read(buf, n, i);
  [[cst::proof]] { /* pure-fact glue: inth i (replace_inth i ch xs) == ch */ }
  return got;
}
#include "psi_examples/units/char_array_unit.h"
#require "psi_examples/units/char_array_unit.c"
char write_then_read(char *buf, int n, int i, char ch)
    [[cst::param(`xs:(int)list`)]]
    [[cst::require(`char_array buf xs ** fact(n == ilength xs)
                    ** fact(0i <= i) ** fact(i < n)`)]]
    [[cst::ensure(`char_array buf (replace_inth i ch xs)
                   ** fact(__return == ch)`)]]
{
  char_array_write(buf, n, i, ch);
  [[cst::proof]] { /* pure-fact glue: replace_inth preserves ilength */ }
  char got = char_array_read(buf, n, i);
  [[cst::proof]] { /* pure-fact glue: inth i (replace_inth i ch xs) == ch */ }
  return got;
}

组合这两次调用时，客户端只需证明关于列表的性质：replace_inthreplace_inth 保持长度不变（因此读操作的前置条件对更新后的列表仍然成立），以及读取更新后的列表在索引 ii 处的元素会得到 chch。两个省略了内容的证明块用该单元导出的引理卸除这些义务，每个只需几行代码。客户端自始至终不接触堆：没有 data_atdata_at 或空洞，也没有折叠。这些推理已在胶囊内部一次性完成。

链表胶囊套件

数组适合作为入门的例子，因为两个胶囊在前置条件和后置条件中都能保持同一抽象视图。链表胶囊的设计则更值得探讨：下面的单元基于我们熟悉的 sllsll 谓词提供四个访问器，每个访问器都需要作出不同的设计选择。

int          read_head (struct list *p) SLL_READ_HEAD_SPEC;
void         write_head(struct list *p, int x) SLL_WRITE_HEAD_SPEC;
struct list *read_tail (struct list *p) SLL_READ_TAIL_SPEC;
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC;
int          read_head (struct list *p) SLL_READ_HEAD_SPEC;
void         write_head(struct list *p, int x) SLL_WRITE_HEAD_SPEC;
struct list *read_tail (struct list *p) SLL_READ_TAIL_SPEC;
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC;

四个访问器只用到两个操作，各自在单元中声明一次：展开操作将非空 sllsll 打开为头单元、尾单元和后继链表，折叠操作则将它们重新组合起来。有一个细节值得注意：每个胶囊的前置条件都将链表写作 cons 形式——sll p (h :: t)sll p (h :: t)——因此展开操作按模式匹配该形状，无需单独的非空前提。这个前提反而由展开操作产出，即 fact(~(p == 0i))fact(~(p == 0i))，随后再由折叠操作消耗。两个操作的义务就这样衔接起来。

保持在同一层次：read_headread_head 与 write_headwrite_head。两个契约的前置条件和后置条件都保持 sllsll：

#define SLL_READ_HEAD_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`sll p (h :: t) ** fact(__return == h)`)]]
int read_head(struct list *p) SLL_READ_HEAD_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  int v = p->head;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return v;
}
#define SLL_READ_HEAD_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`sll p (h :: t) ** fact(__return == h)`)]]
int read_head(struct list *p) SLL_READ_HEAD_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  int v = p->head;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return v;
}

读取操作直接访问普通的 data_atdata_at 单元，随后折叠操作恢复 sll p__pre (h :: t)sll p__pre (h :: t)。从客户端看，调用前后是同一条链表，另外还得到一条纯事实：返回值就是链表的头部值。 write_headwrite_head 以相同的三明治结构包裹 p->head = x;p->head = x;，保证 sll p (x :: t)sll p (x :: t)。

被迫下降一个层次：read_tailread_tail。 read_tailread_tail 应该对返回值承诺什么？在 sllsll 的定义中，尾指针由存在量词绑定，调用方没有可用来引用它的名称。返回尾指针就意味着将它公开，这一选择会体现在契约上：一旦调用方持有尾指针的值，就不能再将该节点隐藏在 sll p (h :: t)sll p (h :: t) 中，否则同一资源会被描述两次。因此，后置条件需要将暴露后的视图交给调用方，并用 __return__return 作为例证：

#define SLL_READ_TAIL_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`data_at (field_addr p Tlist Fhead) Tint h ** data_at (field_addr p Tlist Ftail) Tptr __return ** sll __return t`)]]
#define SLL_READ_TAIL_SPEC                                                    \
  [[cst::param(`h:int`, `t:(int)list`)]]                                      \
  [[cst::require(`sll p (h :: t)`)]]                                          \
  [[cst::ensure(`data_at (field_addr p Tlist Fhead) Tint h ** data_at (field_addr p Tlist Ftail) Tptr __return ** sll __return t`)]]

函数体只做一次展开和一次裸读取，有意省去折叠，目的就是让视图下降一个层次。调用 read_tailread_tail 的客户端此后必须在自己的契约中保留暴露后的节点视图（或者自行将其折叠回去）。这里的关键是选择胶囊后置条件所在的层次；这个接口之所以有用，正是因为它处于较低的层次。

清点每一份资源：write_tailwrite_tail。最具启发性的是最后一个胶囊。将 p->tailp->tail 重新指向另一个链表，只需一次指针存储；但这样会使旧的尾链表成为孤立内存，而分离逻辑不允许已拥有的内存悄然消失。契约必须说明旧尾链表的去向，自然的答案是：作为返回值交还给调用方。

#define SLL_WRITE_TAIL_SPEC                                                   \
  [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]                      \
  [[cst::require(`sll p (h :: t) ** sll new_tail t2`)]]                       \
  [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  struct list *old_tail = p->tail;
  p->tail = new_tail;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return old_tail;
}
#define SLL_WRITE_TAIL_SPEC                                                   \
  [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]                      \
  [[cst::require(`sll p (h :: t) ** sll new_tail t2`)]]                       \
  [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
struct list *write_tail(struct list *p, struct list *new_tail) SLL_WRITE_TAIL_SPEC
{
  [[cst::proof]] { unfold_sll(`p__pre:addr`, `q0:addr`); }
  struct list *old_tail = p->tail;
  p->tail = new_tail;
  [[cst::proof]] { fold_sll(`p__pre:addr`); }
  return old_tail;
}

两条裸语句执行之后，状态中同时保存着重定向后的节点和分离出来的旧尾链表：

折叠操作消耗节点的两个单元以及 sll new_tail__pre t2sll new_tail__pre t2，得到 sll p__pre (h :: t2)sll p__pre (h :: t2)，同时保留独立存在的 sll q0 tsll q0 t 供 returnreturn 使用。注意，参与折叠的是哪条链表，取决于尾单元的当前值：

将四个访问器并列对比：

胶囊 契约层次（前 ->-> 后） 客户端得知或获得的内容
read_headread_head sllsll ->-> sllsll 头部值，以纯事实的形式
write_headwrite_head sllsll ->-> sllsll 同一条链表，头部已被替换
read_tailread_tail sllsll ->-> 暴露的节点 尾指针，以及相应的节点视图
write_tailwrite_tail sll ** sllsll ** sll ->-> sll ** sllsll ** sll 重新拼接的链表，加上旧尾链表的所有权

使用该套件的客户端代码与普通的 C 代码无异。下面的尾交换包装函数在验证时不需要任何证明代码，引擎将幽灵参数 hh、tt、t2t2 与调用方自身的资源合一，自动匹配后置条件：

#include "psi_examples/units/sll_unit.h"
#require "psi_examples/units/sll_unit.c"
struct list *tail_swap(struct list *p, struct list *q)
    [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]
    [[cst::require(`sll p (h :: t) ** sll q t2`)]]
    [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
{
  struct list *old = write_tail(p, q);
  return old;
}
#include "psi_examples/units/sll_unit.h"
#require "psi_examples/units/sll_unit.c"
struct list *tail_swap(struct list *p, struct list *q)
    [[cst::param(`h:int`, `t:(int)list`, `t2:(int)list`)]]
    [[cst::require(`sll p (h :: t) ** sll q t2`)]]
    [[cst::ensure(`sll p (h :: t2) ** sll __return t`)]]
{
  struct list *old = write_tail(p, q);
  return old;
}

经过证明，而非仅凭信任

用安全接口封装不安全的内部实现并不是新想法，Rust 标准库及其生态就是依据这一准则构建的。仔细比较两者，可以看清胶囊进一步提供了什么保证。

安全的 Rust 抽象遵循一个三段式模式：定义一个类型，使它携带编译器无法识别的不变式；将字段设为私有，并逐一审查可能破坏不变式的方法，以强制该不变式成立；在正确性依赖于这个不变式的代码中消费它。当内部必须执行编译器无法检查的操作时，作者写下 unsafeunsafe，并以自然语言记录其推理：

/// # Safety
///
/// `MyHandle` owns its buffer exclusively, so it may be
/// transferred across threads.
unsafe impl Send for MyHandle {}
/// # Safety
///
/// `MyHandle` owns its buffer exclusively, so it may be
/// transferred across threads.
unsafe impl Send for MyHandle {}

从外部看，这一模式运作得相当出色：安全的客户端代码无法破坏不变式，模块边界成为安全边界。不过，这一边界内的保证依赖什么？ /// # Safety/// # Safety 注释是自然语言；unsafe implunsafe impl 是凭声明接受的。编译器采信作者的说法，而模块内部一个细微的错误会悄无声息地使每个安全客户端的保证失效。

PSI 胶囊遵循相同的接口规则：任何客户端调用都由契约保障安全。在此基础上，胶囊内部本身也经过了证明。胶囊函数体中的证明块不是注释；它们会被逐步检查，直至 HOL Light 内核。单元通过验证，就意味着有一条经机器检查的定理，保证裸语句从任何满足前置条件的状态出发执行，都能重新建立后置条件，其中包括恢复不变式和重新折叠。

unsafeunsafe 之上的安全抽象（Rust） PSI 胶囊（C*）
安全性质的陈述位置 自然语言的 /// # Safety/// # Safety 注释 契约宏，机器可读
内部正确性 经人工审计后予以信任 已证明；经内核检查
内部出错意味着 日后某个客户端出现未定义行为 验证当即在胶囊处失败
客户端的义务 针对安全 API 通过类型检查 符号状态匹配前置条件

胶囊无法应用时

胶囊调用的验证方式与任何契约调用相同：引擎将当前符号状态与前置条件匹配。匹配失败时，错误信息会显示出错的语句，以 ▸▸ 标记该语句，并给出它在调用方中的位置和该处的符号状态。调用处的失败大多属于以下几种情况，可以直接根据错误信息辨认：

症状 首先检查
找不到空间资源 状态是否处于胶囊所在的层次？仍处于折叠状态（或已展开到更低层次）的视图必须先调整到契约所在的层次——或者改选发布在当前层次上的胶囊。
纯前置条件未卸除 该分支是否以显式合取项的形式携带了所需的 fact(...)fact(...)——边界事实、非空事实？应在调用前先建立它。
后置条件中的存在量化义务未能卸除 引擎通过匹配 data_atdata_at 来实例化例证；若有遗留义务，通常是例证的语法形式还差一次重写。
验证器报告资源泄漏 该调用丢弃了契约规定由调用方拥有的内存（旧尾链表、分离出来的节点）。消耗或返回它；分离逻辑不允许它凭空消失。

本节开头描述的那种错误不会再出现在调用处：手写的展开-折叠代码有许多副本，其中一份出现了细微错误。现在这份证明只保留在胶囊内部一处，且已经通过检查。

小结

  • 一个 PSI 胶囊将实现、规约和证明组织为一个带契约的 C 函数；三种产物共同演进，声明与定义共享的契约宏保证接口与义务一致。
  • 函数体是一个证明三明治（打开抽象层、一两条裸语句、折叠回去），由操作式风格的可复用操作构造而成。
  • 客户端通过 #include#include + #require#require 接入胶囊，以普通 C 形式调用；展开-折叠推理在胶囊内部完成一次，而非在调用处重复。
  • 胶囊发布在谓词层次中的特定层次上，调用方选择与当前符号状态匹配的胶囊。
  • 与建立在 unsafeunsafe 之上的安全封装相比，胶囊保留了安全接口，并将依靠信任的自然语言说明替换为经内核检查的证明；引擎和描述外部世界的规约仍然属于可信计算基。