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;                // 声明复用该宏
          // 以及客户端声明自己的规约所需的谓词导出
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;                // 声明复用该宏
          // 以及客户端声明自己的规约所需的谓词导出
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 告知验证器（已通过验证的）定义所在的位置。 之后，调用胶囊就是依据其契约进行符号执行——与调用任何契约函数完全相同。

胶囊位于谓词层次中的特定层次上。 像 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 表示元素 ii 被替换为 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 将 hole 和更新后的单元折叠回完整的数组，把逐点的存储转变为一次列表更新：

该最终状态与后置条件匹配，胶囊通过验证，不遗留任何 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 "char_array_unit.h"
#require "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 "char_array_unit.h"
#require "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、没有 hole、没有折叠。 这些推理已在胶囊内部一次性完成。

链表胶囊套件

数组是较为平缓的起点，因为两个胶囊在契约两侧都能保持同一抽象视图。 链表则让胶囊设计真正变得有趣：下面的单元基于熟悉的 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 "sll_unit.h"
#require "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 "sll_unit.h"
#require "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 之上的安全封装，胶囊保留了安全接口，但将被信任的自然语言替换为经内核检查的证明——同时如实承认引擎和面向外部世界的规约仍然属于可信计算基。