C*：开发与证明一体化

用 SMT 求解纯目标

EN | 中文

上一节最后通过纯化得到了普通逻辑目标，包括 reversereverse 循环头部的列表等式 l = REVERSE [] ++ ll = REVERSE [] ++ l；完成数组示例后，还会得到 clearclear 中的索引边界与 replace_inthreplace_inth 等式。等式、整数运算以及涉及这些运算的量化事实，正是 SMT 求解器擅长处理的内容。本节将 C* 的证明层连接到 Z3，用 SMT_TACSMT_TAC 解决这些目标，并将三个步骤组合为完整的流水线。在两个示例的程序点上，只需调用这条流水线就能完成证明。

配置 Z3

SMT 用户库通过 Z3 的 C API 调用求解器，因此需要安装带 C 头文件与链接库的 Z3；安装方式因平台而异。安装后，在仓库根目录的 cstar.tomlcstar.toml 中将构建系统指向 Z3 的安装位置：

cflags = "-I/path/to/z3/include"
link_flags = "-L/path/to/z3/lib -lz3"
cflags = "-I/path/to/z3/include"
link_flags = "-L/path/to/z3/lib -lz3"

/path/to/z3/path/to/z3 需要替换为本机上的实际路径。如果 Z3 位于编译器的默认搜索路径中，只需设置 link_flags = "-lz3"link_flags = "-lz3"（策略示例采用的就是这种配置）。cstarccstarc 只会将自身的头文件目录、库目录以及项目根目录加入编译器的搜索路径。如果 Z3 的安装前缀不在随附 clangclang 的默认搜索范围内，比如从源码编译后安装到 /opt/z3/opt/z3，就需要显式给出 -I-I 与 -L-L 路径。要快速检查环境，可以验证完整的示例：

cstarc verify strategy_demo/examples/reverse.c
cstarc verify strategy_demo/examples/clear.c
cstarc verify strategy_demo/examples/reverse.c
cstarc verify strategy_demo/examples/clear.c

SMT_TACSMT_TAC

PROOF gnode SMT_TAC(gnode gn);
PROOF gnode SMT_TAC(gnode gn);

SMT_TACSMT_TAC 把当前的普通 HOL 目标交给已初始化的 SMT 用户库。如果 Z3 判定目标有效，SMT_TACSMT_TAC 就会求解当前 gnodegnode；如果翻译失败、求解器无法判定，或目标本身无效，目标就会保持开放，由用户继续处理。

有了 PURIFY_TACPURIFY_TAC、POST_PURIFY_TACPOST_PURIFY_TAC 与 SMT_TACSMT_TAC 这三个策略，就可以将本部分的流水线封装为一个可复用的函数：

PROOF thm solve_vc_auto(term vc) {
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  SMT_TAC(g);
  return gnode_prove(root);
}
PROOF thm solve_vc_auto(term vc) {
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  SMT_TAC(g);
  return gnode_prove(root);
}

在需要重建不变式或建立后置条件状态的程序点上，都可以先读取符号状态，再构造蕴含，最后提交证明得到的定理：

PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}
PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

完整示例 strategy_demo/examples/reverse.cstrategy_demo/examples/reverse.c 中的函数与 reverse_clean.creverse_clean.c 相同，只是删去了那条很长的断言。它在三个位置调用 solve_vc_autosolve_vc_auto：循环前建立不变式，循环体末尾重建不变式，循环结束后将状态转换为 returnreturn 所需的形式：

PROOF {
  term st = cst_get_symbolic_state();
  term return_ready = `exists t_v v_v w_v.
    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 (REVERSE l)
  `;
  term vc = `${st:hprop} |-- ${return_ready:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}
PROOF {
  term st = cst_get_symbolic_state();
  term return_ready = `exists t_v v_v w_v.
    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 (REVERSE l)
  `;
  term vc = `${st:hprop} |-- ${return_ready:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

这里仍然通过定理更新状态：solve_vc_autosolve_vc_auto 返回一条蕴含定理，再由 cst_set_symbolic_statecst_set_symbolic_state 提交，整个过程不会直接修改状态。

告诉求解器必要的列表知识

SMT 求解器擅长处理等式、整数运算和量词，但 Z3 的内建知识并不包含 REVERSEREVERSE 的 HOL 定义或 REVERSE_REVERSEREVERSE_REVERSE 定理。 smt_add_axiomsmt_add_axiom 可以将这些已经证明的定理作为背景知识，供后续 SMT 调用使用。reverse.creverse.c 在加载时将它们一次性注册：

PROOF static int install_smt(void) {
  smt_init();
  smt_register_seq_handler();
  type_pair_list int_inst = (type_pair_list)vector_create();
  vector_add(&int_inst, ((type_pair){`:int`, `:A`}));
  thm reverse_def_int = gen_all_rule(
    inst_type_rule(int_inst, get_REVERSE()));
  thm reverse_reverse_int = gen_all_rule(inst_type_rule(
    int_inst, get_theorem_by_name("REVERSE_REVERSE")));
  smt_add_axiom(reverse_def_int);
  smt_add_axiom(reverse_reverse_int);
  return 0;
}
PROOF static int _install_smt = install_smt();
PROOF static int install_smt(void) {
  smt_init();
  smt_register_seq_handler();
  type_pair_list int_inst = (type_pair_list)vector_create();
  vector_add(&int_inst, ((type_pair){`:int`, `:A`}));
  thm reverse_def_int = gen_all_rule(
    inst_type_rule(int_inst, get_REVERSE()));
  thm reverse_reverse_int = gen_all_rule(inst_type_rule(
    int_inst, get_theorem_by_name("REVERSE_REVERSE")));
  smt_add_axiom(reverse_def_int);
  smt_add_axiom(reverse_reverse_int);
  return 0;
}
PROOF static int _install_smt = install_smt();

核心调用是 smt_add_axiomsmt_add_axiom：其参数是一条定理，定理的结论将成为求解器可用的背景知识。定理的假设会先被卸除，但自由项变量不会被全称化，因此需要显式调用 gen_all_rulegen_all_rule。还需要一个技术步骤：单态化（monomorphization）。 HOL 列表定理是多态的，其中的元素类型 AA 尚未固定。当前的翻译过程不支持 HOL 多态，因此需要先用 inst_type_ruleinst_type_rule 将 AA 固定为此处实际使用的 intint，再将定理交给求解器。

term_to_z3term_to_z3 内部

SMT_TACSMT_TAC 位于 userlib/smt/smt.cuserlib/smt/smt.c，其核心做法是递归检查 HOL 项的结构，构建语义上对应的 Z3 AST。 term_to_z3term_to_z3 的主体可以概括为：

Z3_ast term_to_z3(Z3_context ctx, term tm) {
  if (is_int(tm))
    return Z3_mk_int(ctx, dest_int(tm), Z3_mk_int_sort(ctx));
  if (is_forall(tm)) {
    /* 翻译绑定变量的类型，递归进入主体，构建 Z3 forall */
  }
  if (is_exists(tm)) {
    /* 类似地，构建 Z3 exists */
  }
  if (is_var(tm)) {
    /* 自由变量变为同名、同类型的 Z3 常量 */
  }
  if (is_const(tm) || is_comb(tm))
    return smt_app_to_z3(ctx, tm);
  return NULL;
}
Z3_ast term_to_z3(Z3_context ctx, term tm) {
  if (is_int(tm))
    return Z3_mk_int(ctx, dest_int(tm), Z3_mk_int_sort(ctx));
  if (is_forall(tm)) {
    /* 翻译绑定变量的类型，递归进入主体，构建 Z3 forall */
  }
  if (is_exists(tm)) {
    /* 类似地，构建 Z3 exists */
  }
  if (is_var(tm)) {
    /* 自由变量变为同名、同类型的 Z3 常量 */
  }
  if (is_const(tm) || is_comb(tm))
    return smt_app_to_z3(ctx, tm);
  return NULL;
}

函数应用（application）按头部常量分发：==>==> 变为 Z3_mk_impliesZ3_mk_implies，/\/\ 变为 Z3_mk_andZ3_mk_and，整数 ++、--、**、<<、<=<= 映射到相应的 Z3 运算。类型可翻译的其他函数则作为未解释函数（uninterpreted function）处理；smt_add_axiomsmt_add_axiom 添加的定理用来约束它们的行为。 smt_register_seq_handlersmt_register_seq_handler 注册的处理器还会将列表相关的符号映射到 Z3 的序列理论：NILNIL 映射为空序列，CONSCONS 与 APPENDAPPEND 映射为序列拼接，inthinth 映射为序列索引，类型 (A)list(A)list 映射为序列类型。因此，列表目标中的这些符号在 Z3 中都有对应的解释。

最后，求解器断言背景知识与目标的否定。如果 Z3 报告不可满足（unsatisfiable），则反模型（countermodel）不存在，目标有效，SMT_TACSMT_TAC 据此求解该 gnodegnode。

完成 clearclear

数组示例 strategy_demo/examples/clear.cstrategy_demo/examples/clear.c 把 00 写入数组的每一个元素。上一节的策略已经能够处理其中的空间推理，剩下的纯目标涉及 replace_inthreplace_inth，也就是 int_array_with_holeint_array_with_hole 规则引入逻辑列表中的函数。下面三条引理已在 strategy_demo/array/lemmas.cstrategy_demo/array/lemmas.c 中一次性证明，准确刻画了一次更新对读取结果和列表长度的影响：

|- forall i v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     inth i (replace_inth i v l) = v
|- forall i j v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     0i <= j ==> j < ilength l ==> ~(j = i) ==>
     inth j (replace_inth i v l) = inth j l
|- forall i v:int. forall l:(int)list.
     ilength (replace_inth i v l) = ilength l
|- forall i v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     inth i (replace_inth i v l) = v
|- forall i j v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     0i <= j ==> j < ilength l ==> ~(j = i) ==>
     inth j (replace_inth i v l) = inth j l
|- forall i v:int. forall l:(int)list.
     ilength (replace_inth i v l) = ilength l

clear.cclear.c 安装数组策略，并将这三条引理注册为 SMT 背景知识，然后用两个证明块完成验证：一个位于循环体末尾，另一个位于循环之后，将状态转换为后置条件的形式：

PROOF static int _strategy_demo_array = install_strategy_demo_array();
PROOF static int install_clear_smt_axioms(void) {
  smt_add_axiom(replace_inth_at());
  smt_add_axiom(replace_inth_other());
  smt_add_axiom(replace_inth_length());
  return 0;
}
PROOF static int _clear_smt_axioms = install_clear_smt_axioms();
void clear(int *to, int len)
  [[cst::require(`exists l.
    fact(0i <= len && len <= 100i) **
    fact(ilength l == len) **
    int_array to 0i len l
  `)]]
  [[cst::ensure(`exists l.
    fact(forall i. 0i <= i && i < len ==> inth i l = 0i) **
    int_array to 0i len l
  `)]]
{
  int i = 0;
  PROOF term loop_inv = `exists i_v l.
    fact(0i <= i_v && i_v <= len__pre &&
         0i <= len__pre && len__pre <= 100i && ilength l == len__pre) **
    fact(forall j. 0i <= j && j < i_v ==> inth j l = 0i) **
    data_at to__addr Tptr to__pre **
    data_at len__addr Tint len__pre **
    data_at i__addr Tint i_v **
    int_array to__pre 0i len__pre l
  `;
  while (i < len)
    [[cst::invariant(loop_inv)]]
  {
    to[i] = 0;
    i = i + 1;
    PROOF {
      term st = cst_get_symbolic_state();
      term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
      cst_set_symbolic_state(solve_vc_auto(vc));
    }
  }
  PROOF {
    term st = cst_get_symbolic_state();
    term post_ready = `exists i_v l.
      fact(forall i. 0i <= i && i < len__pre ==> inth i l = 0i) **
      data_at to__addr Tptr to__pre **
      data_at len__addr Tint len__pre **
      data_at i__addr Tint i_v **
      int_array to__pre 0i len__pre l
    `;
    term vc = `${st:hprop} |-- ${post_ready:hprop}`;
    cst_set_symbolic_state(solve_vc_auto(vc));
  }
}
PROOF static int _strategy_demo_array = install_strategy_demo_array();
PROOF static int install_clear_smt_axioms(void) {
  smt_add_axiom(replace_inth_at());
  smt_add_axiom(replace_inth_other());
  smt_add_axiom(replace_inth_length());
  return 0;
}
PROOF static int _clear_smt_axioms = install_clear_smt_axioms();
void clear(int *to, int len)
  [[cst::require(`exists l.
    fact(0i <= len && len <= 100i) **
    fact(ilength l == len) **
    int_array to 0i len l
  `)]]
  [[cst::ensure(`exists l.
    fact(forall i. 0i <= i && i < len ==> inth i l = 0i) **
    int_array to 0i len l
  `)]]
{
  int i = 0;
  PROOF term loop_inv = `exists i_v l.
    fact(0i <= i_v && i_v <= len__pre &&
         0i <= len__pre && len__pre <= 100i && ilength l == len__pre) **
    fact(forall j. 0i <= j && j < i_v ==> inth j l = 0i) **
    data_at to__addr Tptr to__pre **
    data_at len__addr Tint len__pre **
    data_at i__addr Tint i_v **
    int_array to__pre 0i len__pre l
  `;
  while (i < len)
    [[cst::invariant(loop_inv)]]
  {
    to[i] = 0;
    i = i + 1;
    PROOF {
      term st = cst_get_symbolic_state();
      term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
      cst_set_symbolic_state(solve_vc_auto(vc));
    }
  }
  PROOF {
    term st = cst_get_symbolic_state();
    term post_ready = `exists i_v l.
      fact(forall i. 0i <= i && i < len__pre ==> inth i l = 0i) **
      data_at to__addr Tptr to__pre **
      data_at len__addr Tint len__pre **
      data_at i__addr Tint i_v **
      int_array to__pre 0i len__pre l
    `;
    term vc = `${st:hprop} |-- ${post_ready:hprop}`;
    cst_set_symbolic_state(solve_vc_auto(vc));
  }
}

循环体执行一次时，证明按以下步骤推进：

  1. 符号执行准备执行 to[i] = 0to[i] = 0，需要目标单元的 data_atdata_at；
  2. 数组规则 00 从 int_arrayint_array 中切出该单元，留下 int_array_with_holeint_array_with_hole。由于不变式中的事实给出了 0 <= i_v0 <= i_v 与 i_v < len__prei_v < len__pre，规则的两条 inferinfer 检查都能通过；
  3. 执行写入后，该单元的值变为 00；
  4. 重建不变式时，规则 11 把左侧的空洞与右侧的目标 int_arrayint_array 匹配，将目标改写为一个存在变量 vv、索引 ii 处的 data_atdata_at，以及等式 l2 = replace_inth (i - x) v l1l2 = replace_inth (i - x) v l1；
  5. 通用 data_atdata_at 策略将刚写入的单元与这个 data_atdata_at 一同消去，并实例化 v = 0v = 0；
  6. 如果状态两侧都直接包含同一区段的 int_arrayint_array，就可以用规则 22 消去空间谓词，留下列表等式；
  7. POST_PURIFY_TACPOST_PURIFY_TAC 生成普通逻辑目标，SMT_TACSMT_TAC 再利用 replace_inthreplace_inth 引理，证明已清零的前缀增加了一个单元，长度与边界事实仍然成立。

循环入口不需要证明块：注册策略后，引擎可以自行建立不变式。后置条件则需要单独的证明块。循环结束后，状态中仍然包含不变式中的 i_vi_v，以及退出循环时的事实 i_v >= len__prei_v >= len__pre。引擎内置的求解器不会自行将不变式中的 forall j. … j < i_v …forall j. … j < i_v … 转换为后置条件中的 forall i. … i < len__pre …forall i. … i < len__pre …，因此这条蕴含会作为尚未解决的验证条件保留下来。第二个证明块用 post_readypost_ready 表示后置条件所需的状态，再调用 solve_vc_autosolve_vc_auto，由 SMT_TACSMT_TAC 完成这一步量词推理。

自动化的局限

小结

  • SMT_TACSMT_TAC 将普通 HOL 目标连同已注册的背景定理翻译到 Z3，通过断言目标的否定，以不可满足性判定目标有效，从而解决目标。求解过程有超时限制；求解器的判定结果被直接信任，判定有效的目标列入报告的 axiomsaxioms 数组。
  • smt_add_axiomsmt_add_axiom 把已证明的 HOL 定理转化为求解器的背景知识；多态的列表定理在提交给求解器之前，先用 inst_type_ruleinst_type_rule 单态化，并用 gen_all_rulegen_all_rule 全称化。
  • term_to_z3term_to_z3 根据项的结构递归构建 Z3 AST，按头部常量分发函数应用，将可翻译但含义未知的函数保留为未解释函数；序列处理器将列表相关的符号映射到 Z3 的序列理论。
  • solve_vc_autosolve_vc_auto 依次执行纯化、后纯化和 SMT 求解，在 reversereverse 的三个程序点和 clearclear 的两个程序点上卸除了全部剩余义务。上一节的策略与本节的求解器共同完成了整个证明。
  • 策略内部的 inferinfer 检查与 SMT_TACSMT_TAC 处于不同层次：前者在 QCP 内部判断规则在局部是否适用，后者在 C* 证明层解决整个纯目标。